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 1417 | . 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) | |
5 | 1, 2, 3, 4 | syl3anc 1363 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1078 |
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 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 |
This theorem is referenced by: 3jaodan 1422 3jaao 1424 fntpb 6963 dfwe2 7485 smo11 7990 smoord 7991 omeulem1 8197 omopth2 8199 oaabs2 8261 elfiun 8882 r111 9192 r1pwss 9201 pwcfsdom 9993 winalim2 10106 xmullem 12645 xmulasslem 12666 xlemul1a 12669 xrsupsslem 12688 xrinfmsslem 12689 xrub 12693 ordtbas2 21727 ordtbas 21728 fmfnfmlem4 22493 dyadmbl 24128 scvxcvx 25490 perfectlem2 25733 2sq2 25936 ostth3 26141 satfun 32555 poseq 32992 sltsolem1 33077 lineext 33434 fscgr 33438 colinbtwnle 33476 broutsideof2 33480 lineunray 33505 lineelsb2 33506 elicc3 33562 4atlem11 36625 dalawlem10 36896 3cubeslem1 39159 frege129d 39986 goldbachth 43586 perfectALTVlem2 43764 eenglngeehlnmlem1 44652 eenglngeehlnmlem2 44653 |
Copyright terms: Public domain | W3C validator |