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.2 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
2 | syl6an.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | jctild 564 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 ∧ 𝜃))) |
4 | syl6an.3 | . 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜏) | |
5 | 3, 4 | syl6 34 | 1 ⊢ (𝜑 → (𝜒 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: dfsb2 2361 xpcan 5489 xpcan2 5490 mapxpen 8011 sucdom2 8041 f1finf1o 8072 unfi 8112 inf3lem3 8410 dfac12r 8851 cfsuc 8962 fin23lem26 9030 iundom2g 9241 inar1 9476 rankcf 9478 ltsrpr 9777 supsrlem 9811 axpre-sup 9869 nominpos 11146 ublbneg 11649 qbtwnre 11904 fsequb 12636 fi1uzind 13134 brfi1indALT 13137 fi1uzindOLD 13140 brfi1indALTOLD 13143 rexanre 13934 rexuzre 13940 rexico 13941 caubnd 13946 rlim2lt 14076 rlim3 14077 lo1bddrp 14104 o1lo1 14116 climshftlem 14153 rlimcn2 14169 rlimo1 14195 lo1add 14205 lo1mul 14206 lo1le 14230 isercoll 14246 serf0 14259 cvgcmp 14389 dvds1lem 14831 dvds2lem 14832 isprm5 15257 vdwlem2 15524 vdwlem10 15532 vdwlem11 15533 lsmcv 18962 lmconst 20875 ptcnplem 21234 fclscmp 21644 tsmsres 21757 addcnlem 22475 lebnumlem3 22570 xlebnum 22572 lebnumii 22573 iscmet3lem2 22898 bcthlem4 22932 cniccbdd 23037 ovoliunlem2 23078 mbfi1flimlem 23295 ply1divex 23700 aalioulem3 23893 aalioulem5 23895 aalioulem6 23896 aaliou 23897 ulmshftlem 23947 ulmbdd 23956 tanarg 24169 cxploglim 24504 ftalem2 24600 ftalem7 24605 dchrisumlem3 24980 nvnencycllem 26171 frgraogt3nreg 26647 ubthlem3 27112 spansncol 27811 riesz1 28308 erdsze2lem2 30440 dfrdg4 31228 neibastop2 31526 onsuct0 31610 bj-bary1 32339 topdifinffinlem 32371 poimirlem24 32603 incsequz 32714 caushft 32727 equivbnd 32759 cntotbnd 32765 4atexlemex4 34377 frege124d 37072 gneispace 37452 expgrowth 37556 vk15.4j 37755 sstrALT2 38092 iccpartdisj 39975 ccats1pfxeqrex 40285 av-frgraogt3nreg 41551 |
Copyright terms: Public domain | W3C validator |