Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl6an | Structured version Visualization version GIF version |
Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.) |
Ref | Expression |
---|---|
syl6an.1 | ⊢ (𝜑 → 𝜓) |
syl6an.2 | ⊢ (𝜑 → (𝜒 → 𝜃)) |
syl6an.3 | ⊢ ((𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl6an | ⊢ (𝜑 → (𝜒 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6an.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl6an.2 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
3 | syl6an.3 | . . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏) | |
4 | 3 | ex 413 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) |
5 | 1, 2, 4 | sylsyld 61 | 1 ⊢ (𝜑 → (𝜒 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 |
This theorem is referenced by: dfsb2 2528 dfsb2ALT 2587 xpcan 6027 xpcan2 6028 mapxpen 8672 sucdom2 8703 f1finf1o 8734 unfi 8774 inf3lem3 9082 dfac12r 9561 cfsuc 9668 fin23lem26 9736 iundom2g 9951 inar1 10186 rankcf 10188 ltsrpr 10488 supsrlem 10522 axpre-sup 10580 nominpos 11863 ublbneg 12322 qbtwnre 12582 fsequb 13333 fi1uzind 13845 brfi1indALT 13848 ccats1pfxeqrex 14067 rexanre 14696 rexuzre 14702 rexico 14703 caubnd 14708 rlim2lt 14844 rlim3 14845 lo1bddrp 14872 o1lo1 14884 climshftlem 14921 rlimcn2 14937 rlimo1 14963 lo1add 14973 lo1mul 14974 lo1le 14998 isercoll 15014 serf0 15027 cvgcmp 15161 dvds1lem 15611 dvds2lem 15612 mulmoddvds 15669 isprm5 16041 vdwlem2 16308 vdwlem10 16316 vdwlem11 16317 lsmcv 19844 lmconst 21799 ptcnplem 22159 fclscmp 22568 tsmsres 22681 addcnlem 23401 lebnumlem3 23496 xlebnum 23498 lebnumii 23499 iscmet3lem2 23824 bcthlem4 23859 cniccbdd 23991 ovoliunlem2 24033 mbfi1flimlem 24252 ply1divex 24659 aalioulem3 24852 aalioulem5 24854 aalioulem6 24855 aaliou 24856 ulmshftlem 24906 ulmbdd 24915 tanarg 25129 cxploglim 25483 ftalem2 25579 ftalem7 25584 dchrisumlem3 25995 frgrogt3nreg 28104 ubthlem3 28577 spansncol 29273 riesz1 29770 erdsze2lem2 32349 dfrdg4 33310 neibastop2 33607 onsuct0 33687 bj-bary1 34482 topdifinffinlem 34511 finorwe 34546 poimirlem24 34798 incsequz 34906 caushft 34919 equivbnd 34951 cntotbnd 34957 4atexlemex4 37091 frege124d 39986 gneispace 40364 expgrowth 40547 vk15.4j 40742 sstrALT2 41049 iccpartdisj 43444 fppr2odd 43743 |
Copyright terms: Public domain | W3C validator |