Theorem syl3c 67

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 66	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
6	1, 5	mpd 16	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  fodomr  9131  dffi3  9407  cantnflt  9657  cantnflem1  9674  axdc3lem2  10510  seqf1olem2  14165  wrd2ind  14852  relexpindlem  15196  rtrclind  15198  o1fsum  15960  lcmneg  16758  prmind2  16840  rami  17173  ramcl  17187  pslem  18726  telgsums  20187  islbs3  21413  psgndif  21888  mplsubglem  22286  mpllsslem  22287  gsummatr01lem4  22953  lmmo  23678  cnmpt12  23966  cnmpt22  23973  filss  24152  flimopn  24274  flimrest  24282  cfil3i  25570  equivcfil  25600  equivcau  25601  ovolicc2lem3  25820  limciun  26194  dvcnvrelem1  26317  dvfsumrlim  26331  dvfsum2  26334  dgrco  26574  scvxcvx  27295  ftalem3  27384  2sqlem6  27732  2sqlem8  27735  dchrisumlema  27797  dchrisumlem2  27799  addsproplem1  28337  negsproplem1  28396  gropd  29591  grstructd  29592  pthdepisspth  30303  pjoi0  32301  atomli  32966  archirng  33731  archiabllem1a  33734  archiabllem2a  33737  archiabl  33741  crefi  34461  pcmplfin  34474  sigaclcu  34731  measvun  34824  signsply0  35163  bnj1128  35603  bnj1204  35625  bnj1417  35654  neibastop2lem  37118  poimirlem31  38537  ftc1cnnclem  38577  sdclem2  38644  heibor1lem  38711  cvrat4  40468  hdmapval2  42857  ismrcd1  43662  relexpxpmin  44676  ee222  45444  ee333  45449  ee1111  45458  sbcoreleleq  45477  ordelordALT  45479  trsbc  45482  ee110  45619  ee101  45621  ee011  45623  ee100  45625  ee010  45627  ee001  45629  eel11111  45664  fnchoice  45989  fiiuncl  46025  mullimc  46572  islptre  46575  mullimcf  46579  addlimc  46602  stoweidlem20  46974  stoweidlem59  47013  perfectALTVlem2  48764