Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3jaodan | Structured version Visualization version GIF version |
Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
3jaodan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3jaodan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
3jaodan.3 | ⊢ ((𝜑 ∧ 𝜏) → 𝜒) |
Ref | Expression |
---|---|
3jaodan | ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3jaodan.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 450 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 3jaodan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
4 | 3 | ex 450 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) |
5 | 3jaodan.3 | . . . 4 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
6 | 5 | ex 450 | . . 3 ⊢ (𝜑 → (𝜏 → 𝜒)) |
7 | 2, 4, 6 | 3jaod 1392 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
8 | 7 | imp 445 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∨ w3o 1036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 |
This theorem is referenced by: onzsl 7046 zeo 11463 xrltnsym 11970 xrlttri 11972 xrlttr 11973 qbtwnxr 12031 xltnegi 12047 xaddcom 12071 xnegdi 12078 xsubge0 12091 xrub 12142 bpoly3 14789 blssioo 22598 ismbf2d 23408 itg2seq 23509 eliccioo 29639 3ccased 31600 lineelsb2 32255 dfxlim2v 40073 |
Copyright terms: Public domain | W3C validator |