![]() |
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 9159 dffi3 9462 cantnflt 9703 cantnflem1 9720 axdc3lem2 10482 seqf1olem2 14047 wrd2ind 14713 relexpindlem 15050 rtrclind 15052 o1fsum 15799 lcmneg 16581 prmind2 16663 rami 16991 ramcl 17005 pslem 18571 telgsums 19955 islbs3 21050 psgndif 21541 mplsubglem 21948 mpllsslem 21949 gsummatr01lem4 22580 lmmo 23304 cnmpt12 23591 cnmpt22 23598 filss 23777 flimopn 23899 flimrest 23907 cfil3i 25217 equivcfil 25247 equivcau 25248 ovolicc2lem3 25468 limciun 25843 dvcnvrelem1 25970 dvfsumrlim 25986 dvfsum2 25989 dgrco 26230 scvxcvx 26938 ftalem3 27027 2sqlem6 27376 2sqlem8 27379 dchrisumlema 27441 dchrisumlem2 27443 addsproplem1 27906 negsproplem1 27960 gropd 28864 grstructd 28865 pthdepisspth 29569 pjoi0 31547 atomli 32212 archirng 32917 archiabllem1a 32920 archiabllem2a 32923 archiabl 32927 crefi 33481 pcmplfin 33494 sigaclcu 33769 measvun 33861 signsply0 34216 bnj1128 34654 bnj1204 34676 bnj1417 34705 neibastop2lem 35877 poimirlem31 37157 ftc1cnnclem 37197 sdclem2 37248 heibor1lem 37315 cvrat4 38948 hdmapval2 41337 ismrcd1 42149 relexpxpmin 43178 ee222 43972 ee333 43977 ee1111 43986 sbcoreleleq 44005 ordelordALT 44007 trsbc 44010 ee110 44147 ee101 44149 ee011 44151 ee100 44153 ee010 44155 ee001 44157 eel11111 44193 fnchoice 44422 fiiuncl 44460 mullimc 45033 islptre 45036 mullimcf 45040 addlimc 45065 stoweidlem20 45437 stoweidlem59 45476 perfectALTVlem2 47091 |
Copyright terms: Public domain | W3C validator |