| 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 1086 |
| 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 849 df-3or 1088 df-3an 1089 |
| This theorem is referenced by: 3jaodan 1433 3jaao 1435 fntpb 7229 dfwe2 7794 poseq 8183 smo11 8404 smoord 8405 omeulem1 8620 omopth2 8622 oaabs2 8687 elfiun 9470 r111 9815 r1pwss 9824 pwcfsdom 10623 winalim2 10736 xmullem 13306 xmulasslem 13327 xlemul1a 13330 xrsupsslem 13349 xrinfmsslem 13350 xrub 13354 fvf1tp 13829 symgvalstruct 19414 symgvalstructOLD 19415 ordtbas2 23199 ordtbas 23200 fmfnfmlem4 23965 dyadmbl 25635 scvxcvx 27029 perfectlem2 27274 2sq2 27477 ostth3 27682 sltsolem1 27720 addsproplem7 28008 negsproplem7 28066 mulsproplem5 28146 mulsproplem6 28147 mulsproplem7 28148 mulsproplem8 28149 satfun 35416 lineext 36077 fscgr 36081 colinbtwnle 36119 broutsideof2 36123 lineunray 36148 lineelsb2 36149 elicc3 36318 4atlem11 39611 dalawlem10 39882 3cubeslem1 42695 dflim5 43342 omabs2 43345 omcl3g 43347 naddwordnexlem4 43414 frege129d 43776 goldbachth 47534 perfectALTVlem2 47709 gpgedgel 48007 gpgusgralem 48011 gpgvtxedg0 48021 gpgvtxedg1 48022 gpgnbgrvtx0 48030 gpgnbgrvtx1 48031 eenglngeehlnmlem1 48658 eenglngeehlnmlem2 48659 |
| Copyright terms: Public domain | W3C validator |