![]() |
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 412 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 3jaodan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | |
4 | 3 | ex 412 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜒)) |
5 | 3jaodan.3 | . . . 4 ⊢ ((𝜑 ∧ 𝜏) → 𝜒) | |
6 | 5 | ex 412 | . . 3 ⊢ (𝜑 → (𝜏 → 𝜒)) |
7 | 2, 4, 6 | 3jaod 1428 | . 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
8 | 7 | imp 406 | 1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1085 |
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 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 |
This theorem is referenced by: mpjao3dan 1431 onzsl 7867 zeo 12702 xrltnsym 13176 xrlttri 13178 xrlttr 13179 qbtwnxr 13239 xltnegi 13255 xaddcom 13279 xnegdi 13287 xsubge0 13300 xrub 13351 bpoly3 16091 blssioo 24831 ismbf2d 25689 itg2seq 25792 eliccioo 32898 3ccased 35699 lineelsb2 36130 sticksstones1 42128 dfxlim2v 45803 usgrexmpl2trifr 47932 |
Copyright terms: Public domain | W3C validator |