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  8864  dffi3  9120  cantnflt  9360  cantnflem1  9377  axdc3lem2  10138  seqf1olem2  13691  wrd2ind  14364  relexpindlem  14702  rtrclind  14704  o1fsum  15453  lcmneg  16236  prmind2  16318  rami  16644  ramcl  16658  pslem  18205  telgsums  19509  islbs3  20332  psgndif  20719  mplsubglem  21115  mpllsslem  21116  gsummatr01lem4  21715  lmmo  22439  cnmpt12  22726  cnmpt22  22733  filss  22912  flimopn  23034  flimrest  23042  cfil3i  24338  equivcfil  24368  equivcau  24369  ovolicc2lem3  24588  limciun  24963  dvcnvrelem1  25086  dvfsumrlim  25100  dvfsum2  25103  dgrco  25341  scvxcvx  26040  ftalem3  26129  2sqlem6  26476  2sqlem8  26479  dchrisumlema  26541  dchrisumlem2  26543  gropd  27304  grstructd  27305  pthdepisspth  28004  pjoi0  29980  atomli  30645  archirng  31344  archiabllem1a  31347  archiabllem2a  31350  archiabl  31354  crefi  31699  pcmplfin  31712  sigaclcu  31985  measvun  32077  signsply0  32430  bnj1128  32870  bnj1204  32892  bnj1417  32921  neibastop2lem  34476  poimirlem31  35735  ftc1cnnclem  35775  sdclem2  35827  heibor1lem  35894  cvrat4  37384  hdmapval2  39773  ismrcd1  40436  relexpxpmin  41214  ee222  42011  ee333  42016  ee1111  42025  sbcoreleleq  42044  ordelordALT  42046  trsbc  42049  ee110  42186  ee101  42188  ee011  42190  ee100  42192  ee010  42194  ee001  42196  eel11111  42232  fnchoice  42461  fiiuncl  42502  mullimc  43047  islptre  43050  mullimcf  43054  addlimc  43079  stoweidlem20  43451  stoweidlem59  43490  perfectALTVlem2  45062