![]() |
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: syl1111anc 873 fodomr 8386 dffi3 8612 cantnflt 8853 cantnflem1 8870 axdc3lem2 9595 seqf1olem2 13142 wrd2ind 13821 wrd2indOLD 13822 relexpindlem 14187 rtrclind 14189 o1fsum 14926 lcmneg 15696 prmind2 15777 rami 16097 ramcl 16111 pslem 17566 telgsums 18751 islbs3 19523 mplsubglem 19802 mpllsslem 19803 psgndif 20315 gsummatr01lem4 20840 lmmo 21562 cnmpt12 21848 cnmpt22 21855 filss 22034 flimopn 22156 flimrest 22164 cfil3i 23444 equivcfil 23474 equivcau 23475 ovolicc2lem3 23692 limciun 24064 dvcnvrelem1 24186 dvfsumrlim 24200 dvfsum2 24203 dgrco 24437 scvxcvx 25132 ftalem3 25221 2sqlem6 25568 2sqlem8 25571 dchrisumlema 25597 dchrisumlem2 25599 gropd 26336 grstructd 26337 pthdepisspth 27044 pjoi0 29127 atomli 29792 archirng 30283 archiabllem1a 30286 archiabllem2a 30289 archiabl 30293 crefi 30455 pcmplfin 30468 sigaclcu 30721 measvun 30813 signsply0 31171 bnj1128 31600 bnj1204 31622 bnj1417 31651 noprefixmo 32382 neibastop2lem 32888 poimirlem31 33979 ftc1cnnclem 34021 sdclem2 34075 heibor1lem 34145 cvrat4 35513 hdmapval2 37902 ismrcd1 38100 relexpxpmin 38845 ee222 39541 ee333 39546 ee1111 39555 sbcoreleleq 39574 ordelordALT 39576 trsbc 39579 ee110 39725 ee101 39727 ee011 39729 ee100 39731 ee010 39733 ee001 39735 eel11111 39772 fnchoice 40001 fiiuncl 40046 mullimc 40637 islptre 40640 mullimcf 40644 addlimc 40669 stoweidlem20 41025 stoweidlem59 41064 perfectALTVlem2 42475 |
Copyright terms: Public domain | W3C validator |