Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3jaod | Structured version Visualization version Unicode 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 1389 | . 2 | |
5 | 1, 2, 3, 4 | syl3anc 1326 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 w3o 1036 |
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 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 |
This theorem is referenced by: 3jaodan 1394 3jaao 1396 fntpb 6473 dfwe2 6981 smo11 7461 smoord 7462 omeulem1 7662 omopth2 7664 oaabs2 7725 elfiun 8336 r111 8638 r1pwss 8647 pwcfsdom 9405 winalim2 9518 xmullem 12094 xmulasslem 12115 xlemul1a 12118 xrsupsslem 12137 xrinfmsslem 12138 xrub 12142 ordtbas2 20995 ordtbas 20996 fmfnfmlem4 21761 dyadmbl 23368 scvxcvx 24712 perfectlem2 24955 ostth3 25327 poseq 31750 sltsolem1 31826 lineext 32183 fscgr 32187 colinbtwnle 32225 broutsideof2 32229 lineunray 32254 lineelsb2 32255 elicc3 32311 4atlem11 34895 dalawlem10 35166 frege129d 38055 goldbachth 41459 perfectALTVlem2 41631 |
Copyright terms: Public domain | W3C validator |