![]() |
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 414 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) |
5 | 1, 2, 4 | sylsyld 61 | 1 ⊢ (𝜑 → (𝜒 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: dfsb2 2493 xpcan 6171 xpcan2 6172 sucdom2OLD 9077 mapxpen 9138 sucdom2 9201 f1finf1oOLD 9267 unfiOLD 9308 inf3lem3 9620 dfac12r 10136 nnadju 10187 cfsuc 10247 fin23lem26 10315 iundom2g 10530 inar1 10765 rankcf 10767 ltsrpr 11067 supsrlem 11101 axpre-sup 11159 nominpos 12444 ublbneg 12912 qbtwnre 13173 fsequb 13935 fi1uzind 14453 brfi1indALT 14456 ccats1pfxeqrex 14660 rexanre 15288 rexuzre 15294 rexico 15295 caubnd 15300 rlim2lt 15436 rlim3 15437 lo1bddrp 15464 o1lo1 15476 climshftlem 15513 rlimcn3 15529 rlimo1 15556 lo1add 15566 lo1mul 15567 lo1le 15593 isercoll 15609 serf0 15622 cvgcmp 15757 dvds1lem 16206 dvds2lem 16207 mulmoddvds 16268 isprm5 16639 vdwlem2 16910 vdwlem10 16918 vdwlem11 16919 lsmcv 20741 lmconst 22746 ptcnplem 23106 fclscmp 23515 tsmsres 23629 addcnlem 24361 lebnumlem3 24460 xlebnum 24462 lebnumii 24463 iscmet3lem2 24790 bcthlem4 24825 cniccbdd 24959 ovoliunlem2 25001 mbfi1flimlem 25221 ply1divex 25635 aalioulem3 25828 aalioulem5 25830 aalioulem6 25831 aaliou 25832 ulmshftlem 25882 ulmbdd 25891 tanarg 26108 cxploglim 26461 ftalem2 26557 ftalem7 26562 dchrisumlem3 26973 frgrogt3nreg 29629 ubthlem3 30102 spansncol 30798 riesz1 31295 fineqvac 34034 erdsze2lem2 34132 dfrdg4 34860 neibastop2 35183 onsuct0 35263 bj-bary1 36130 topdifinffinlem 36165 finorwe 36200 poimirlem24 36449 incsequz 36553 caushft 36566 equivbnd 36595 cntotbnd 36601 4atexlemex4 38881 frege124d 42444 gneispace 42817 expgrowth 43026 vk15.4j 43221 sstrALT2 43528 iccpartdisj 46039 fppr2odd 46333 |
Copyright terms: Public domain | W3C validator |