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 13877 wrd2ind 14543 relexpindlem 14882 rtrclind 14884 o1fsum 15633 lcmneg 16414 prmind2 16496 rami 16822 ramcl 16836 pslem 18396 telgsums 19700 islbs3 20540 psgndif 20930 mplsubglem 21328 mpllsslem 21329 gsummatr01lem4 21930 lmmo 22654 cnmpt12 22941 cnmpt22 22948 filss 23127 flimopn 23249 flimrest 23257 cfil3i 24556 equivcfil 24586 equivcau 24587 ovolicc2lem3 24806 limciun 25181 dvcnvrelem1 25304 dvfsumrlim 25318 dvfsum2 25321 dgrco 25559 scvxcvx 26258 ftalem3 26347 2sqlem6 26694 2sqlem8 26697 dchrisumlema 26759 dchrisumlem2 26761 gropd 27781 grstructd 27782 pthdepisspth 28482 pjoi0 30458 atomli 31123 archirng 31819 archiabllem1a 31822 archiabllem2a 31825 archiabl 31829 crefi 32202 pcmplfin 32215 sigaclcu 32490 measvun 32582 signsply0 32937 bnj1128 33376 bnj1204 33398 bnj1417 33427 addsproplem1 34272 negsproplem1 34309 neibastop2lem 34728 poimirlem31 36005 ftc1cnnclem 36045 sdclem2 36097 heibor1lem 36164 cvrat4 37802 hdmapval2 40191 ismrcd1 40887 relexpxpmin 41752 ee222 42549 ee333 42554 ee1111 42563 sbcoreleleq 42582 ordelordALT 42584 trsbc 42587 ee110 42724 ee101 42726 ee011 42728 ee100 42730 ee010 42732 ee001 42734 eel11111 42770 fnchoice 42999 fiiuncl 43038 mullimc 43612 islptre 43615 mullimcf 43619 addlimc 43644 stoweidlem20 44016 stoweidlem59 44055 perfectALTVlem2 45669 |
Copyright terms: Public domain | W3C validator |