| 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 412 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) |
| 5 | 1, 2, 4 | sylsyld 61 | 1 ⊢ (𝜑 → (𝜒 → 𝜏)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 |
| This theorem is referenced by: dfsb2 2498 xpcan 6196 xpcan2 6197 sucdom2OLD 9122 mapxpen 9183 sucdom2 9243 f1finf1oOLD 9306 inf3lem3 9670 dfac12r 10187 nnadju 10238 cfsuc 10297 fin23lem26 10365 iundom2g 10580 inar1 10815 rankcf 10817 ltsrpr 11117 supsrlem 11151 axpre-sup 11209 nominpos 12503 ublbneg 12975 qbtwnre 13241 fsequb 14016 fi1uzind 14546 brfi1indALT 14549 ccats1pfxeqrex 14753 rexanre 15385 rexuzre 15391 rexico 15392 caubnd 15397 rlim2lt 15533 rlim3 15534 lo1bddrp 15561 o1lo1 15573 climshftlem 15610 rlimcn3 15626 rlimo1 15653 lo1add 15663 lo1mul 15664 lo1le 15688 isercoll 15704 serf0 15717 cvgcmp 15852 dvds1lem 16305 dvds2lem 16306 mulmoddvds 16367 isprm5 16744 vdwlem2 17020 vdwlem10 17028 vdwlem11 17029 lsmcv 21143 lmconst 23269 ptcnplem 23629 fclscmp 24038 tsmsres 24152 addcnlem 24886 lebnumlem3 24995 xlebnum 24997 lebnumii 24998 iscmet3lem2 25326 bcthlem4 25361 cniccbdd 25496 ovoliunlem2 25538 mbfi1flimlem 25757 ply1divex 26176 aalioulem3 26376 aalioulem5 26378 aalioulem6 26379 aaliou 26380 ulmshftlem 26432 ulmbdd 26441 tanarg 26661 cxploglim 27021 ftalem2 27117 ftalem7 27122 dchrisumlem3 27535 frgrogt3nreg 30416 ubthlem3 30891 spansncol 31587 riesz1 32084 fineqvac 35111 erdsze2lem2 35209 dfrdg4 35952 neibastop2 36362 onsuct0 36442 weiunpo 36466 bj-bary1 37313 topdifinffinlem 37348 finorwe 37383 poimirlem24 37651 incsequz 37755 caushft 37768 equivbnd 37797 cntotbnd 37803 4atexlemex4 40075 frege124d 43774 gneispace 44147 expgrowth 44354 vk15.4j 44548 sstrALT2 44855 iccpartdisj 47424 fppr2odd 47718 |
| Copyright terms: Public domain | W3C validator |