Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl3c | Structured version Visualization version GIF version |
Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.) |
Ref | Expression |
---|---|
syl3c.1 | ⊢ (𝜑 → 𝜓) |
syl3c.2 | ⊢ (𝜑 → 𝜒) |
syl3c.3 | ⊢ (𝜑 → 𝜃) |
syl3c.4 | ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
Ref | Expression |
---|---|
syl3c | ⊢ (𝜑 → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3c.3 | . 2 ⊢ (𝜑 → 𝜃) | |
2 | syl3c.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | syl3c.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
4 | syl3c.4 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) | |
5 | 2, 3, 4 | sylc 65 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) |
6 | 1, 5 | mpd 15 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: fodomr 9006 dffi3 9301 cantnflt 9542 cantnflem1 9559 axdc3lem2 10321 seqf1olem2 13878 wrd2ind 14544 relexpindlem 14883 rtrclind 14885 o1fsum 15634 lcmneg 16415 prmind2 16497 rami 16823 ramcl 16837 pslem 18397 telgsums 19705 islbs3 20545 psgndif 20935 mplsubglem 21333 mpllsslem 21334 gsummatr01lem4 21935 lmmo 22659 cnmpt12 22946 cnmpt22 22953 filss 23132 flimopn 23254 flimrest 23262 cfil3i 24561 equivcfil 24591 equivcau 24592 ovolicc2lem3 24811 limciun 25186 dvcnvrelem1 25309 dvfsumrlim 25323 dvfsum2 25326 dgrco 25564 scvxcvx 26263 ftalem3 26352 2sqlem6 26699 2sqlem8 26702 dchrisumlema 26764 dchrisumlem2 26766 gropd 27787 grstructd 27788 pthdepisspth 28488 pjoi0 30464 atomli 31129 archirng 31825 archiabllem1a 31828 archiabllem2a 31831 archiabl 31835 crefi 32208 pcmplfin 32221 sigaclcu 32496 measvun 32588 signsply0 32943 bnj1128 33382 bnj1204 33404 bnj1417 33433 addsproplem1 34277 negsproplem1 34314 neibastop2lem 34763 poimirlem31 36040 ftc1cnnclem 36080 sdclem2 36132 heibor1lem 36199 cvrat4 37837 hdmapval2 40226 ismrcd1 40923 relexpxpmin 41788 ee222 42585 ee333 42590 ee1111 42599 sbcoreleleq 42618 ordelordALT 42620 trsbc 42623 ee110 42760 ee101 42762 ee011 42764 ee100 42766 ee010 42768 ee001 42770 eel11111 42806 fnchoice 43035 fiiuncl 43074 mullimc 43648 islptre 43651 mullimcf 43655 addlimc 43680 stoweidlem20 44052 stoweidlem59 44091 perfectALTVlem2 45705 |
Copyright terms: Public domain | W3C validator |