![]() |
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 2492 xpcan 6129 xpcan2 6130 sucdom2OLD 9029 mapxpen 9090 sucdom2 9153 f1finf1oOLD 9219 unfiOLD 9260 inf3lem3 9571 dfac12r 10087 nnadju 10138 cfsuc 10198 fin23lem26 10266 iundom2g 10481 inar1 10716 rankcf 10718 ltsrpr 11018 supsrlem 11052 axpre-sup 11110 nominpos 12395 ublbneg 12863 qbtwnre 13124 fsequb 13886 fi1uzind 14402 brfi1indALT 14405 ccats1pfxeqrex 14609 rexanre 15237 rexuzre 15243 rexico 15244 caubnd 15249 rlim2lt 15385 rlim3 15386 lo1bddrp 15413 o1lo1 15425 climshftlem 15462 rlimcn3 15478 rlimo1 15505 lo1add 15515 lo1mul 15516 lo1le 15542 isercoll 15558 serf0 15571 cvgcmp 15706 dvds1lem 16155 dvds2lem 16156 mulmoddvds 16217 isprm5 16588 vdwlem2 16859 vdwlem10 16867 vdwlem11 16868 lsmcv 20618 lmconst 22628 ptcnplem 22988 fclscmp 23397 tsmsres 23511 addcnlem 24243 lebnumlem3 24342 xlebnum 24344 lebnumii 24345 iscmet3lem2 24672 bcthlem4 24707 cniccbdd 24841 ovoliunlem2 24883 mbfi1flimlem 25103 ply1divex 25517 aalioulem3 25710 aalioulem5 25712 aalioulem6 25713 aaliou 25714 ulmshftlem 25764 ulmbdd 25773 tanarg 25990 cxploglim 26343 ftalem2 26439 ftalem7 26444 dchrisumlem3 26855 frgrogt3nreg 29383 ubthlem3 29856 spansncol 30552 riesz1 31049 fineqvac 33755 erdsze2lem2 33855 dfrdg4 34582 neibastop2 34879 onsuct0 34959 bj-bary1 35829 topdifinffinlem 35864 finorwe 35899 poimirlem24 36148 incsequz 36253 caushft 36266 equivbnd 36295 cntotbnd 36301 4atexlemex4 38582 frege124d 42121 gneispace 42494 expgrowth 42703 vk15.4j 42898 sstrALT2 43205 iccpartdisj 45715 fppr2odd 46009 |
Copyright terms: Public domain | W3C validator |