Theorem syl3c 66

Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)

Hypotheses

Ref	Expression
syl3c.1	⊢ (𝜑 → 𝜓)
syl3c.2	⊢ (𝜑 → 𝜒)
syl3c.3	⊢ (𝜑 → 𝜃)
syl3c.4	⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))

Assertion

Ref	Expression
syl3c	⊢ (𝜑 → 𝜏)

Proof of Theorem 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 ⊢ (𝜑 → 𝜏)

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  8915  dffi3  9190  cantnflt  9430  cantnflem1  9447  axdc3lem2  10207  seqf1olem2  13763  wrd2ind  14436  relexpindlem  14774  rtrclind  14776  o1fsum  15525  lcmneg  16308  prmind2  16390  rami  16716  ramcl  16730  pslem  18290  telgsums  19594  islbs3  20417  psgndif  20807  mplsubglem  21205  mpllsslem  21206  gsummatr01lem4  21807  lmmo  22531  cnmpt12  22818  cnmpt22  22825  filss  23004  flimopn  23126  flimrest  23134  cfil3i  24433  equivcfil  24463  equivcau  24464  ovolicc2lem3  24683  limciun  25058  dvcnvrelem1  25181  dvfsumrlim  25195  dvfsum2  25198  dgrco  25436  scvxcvx  26135  ftalem3  26224  2sqlem6  26571  2sqlem8  26574  dchrisumlema  26636  dchrisumlem2  26638  gropd  27401  grstructd  27402  pthdepisspth  28103  pjoi0  30079  atomli  30744  archirng  31442  archiabllem1a  31445  archiabllem2a  31448  archiabl  31452  crefi  31797  pcmplfin  31810  sigaclcu  32085  measvun  32177  signsply0  32530  bnj1128  32970  bnj1204  32992  bnj1417  33021  neibastop2lem  34549  poimirlem31  35808  ftc1cnnclem  35848  sdclem2  35900  heibor1lem  35967  cvrat4  37457  hdmapval2  39846  ismrcd1  40520  relexpxpmin  41325  ee222  42122  ee333  42127  ee1111  42136  sbcoreleleq  42155  ordelordALT  42157  trsbc  42160  ee110  42297  ee101  42299  ee011  42301  ee100  42303  ee010  42305  ee001  42307  eel11111  42343  fnchoice  42572  fiiuncl  42613  mullimc  43157  islptre  43160  mullimcf  43164  addlimc  43189  stoweidlem20  43561  stoweidlem59  43600  perfectALTVlem2  45174