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 449 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 3jaodan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
4 | 3 | ex 449 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) |
5 | 3jaodan.3 | . . . 4 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
6 | 5 | ex 449 | . . 3 ⊢ (𝜑 → (𝜏 → 𝜒)) |
7 | 2, 4, 6 | 3jaod 1384 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
8 | 7 | imp 444 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∨ w3o 1030 |
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 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 |
This theorem is referenced by: onzsl 6938 zeo 11339 xrltnsym 11846 xrlttri 11848 xrlttr 11849 qbtwnxr 11905 xltnegi 11921 xaddcom 11945 xnegdi 11950 xsubge0 11963 xrub 12014 bpoly3 14628 blssioo 22406 ismbf2d 23214 itg2seq 23315 eliccioo 28970 3ccased 30855 lineelsb2 31425 |
Copyright terms: Public domain | W3C validator |