Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3jaod | Structured version Visualization version GIF version |
Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
3jaod.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
3jaod.2 | ⊢ (𝜑 → (𝜃 → 𝜒)) |
3jaod.3 | ⊢ (𝜑 → (𝜏 → 𝜒)) |
Ref | Expression |
---|---|
3jaod | ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3jaod.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 3jaod.2 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) | |
3 | 3jaod.3 | . 2 ⊢ (𝜑 → (𝜏 → 𝜒)) | |
4 | 3jao 1427 | . 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) | |
5 | 1, 2, 3, 4 | syl3anc 1373 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1088 |
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 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 |
This theorem is referenced by: 3jaodan 1432 3jaao 1435 fntpb 7022 dfwe2 7556 smo11 8098 smoord 8099 omeulem1 8307 omopth2 8309 oaabs2 8371 elfiun 9043 r111 9388 r1pwss 9397 pwcfsdom 10194 winalim2 10307 xmullem 12851 xmulasslem 12872 xlemul1a 12875 xrsupsslem 12894 xrinfmsslem 12895 xrub 12899 symgvalstruct 18786 ordtbas2 22085 ordtbas 22086 fmfnfmlem4 22851 dyadmbl 24494 scvxcvx 25865 perfectlem2 26108 2sq2 26311 ostth3 26516 satfun 33083 poseq 33536 sltsolem1 33612 lineext 34112 fscgr 34116 colinbtwnle 34154 broutsideof2 34158 lineunray 34183 lineelsb2 34184 elicc3 34240 4atlem11 37358 dalawlem10 37629 3cubeslem1 40207 frege129d 41046 goldbachth 44670 perfectALTVlem2 44845 eenglngeehlnmlem1 45754 eenglngeehlnmlem2 45755 |
Copyright terms: Public domain | W3C validator |