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  9041  dffi3  9315  cantnflt  9562  cantnflem1  9579  axdc3lem2  10339  seqf1olem2  13946  wrd2ind  14627  relexpindlem  14967  rtrclind  14969  o1fsum  15717  lcmneg  16511  prmind2  16593  rami  16924  ramcl  16938  pslem  18475  telgsums  19903  islbs3  21090  psgndif  21537  mplsubglem  21934  mpllsslem  21935  gsummatr01lem4  22571  lmmo  23293  cnmpt12  23580  cnmpt22  23587  filss  23766  flimopn  23888  flimrest  23896  cfil3i  25194  equivcfil  25224  equivcau  25225  ovolicc2lem3  25445  limciun  25820  dvcnvrelem1  25947  dvfsumrlim  25963  dvfsum2  25966  dgrco  26206  scvxcvx  26921  ftalem3  27010  2sqlem6  27359  2sqlem8  27362  dchrisumlema  27424  dchrisumlem2  27426  addsproplem1  27910  negsproplem1  27968  gropd  29007  grstructd  29008  pthdepisspth  29711  pjoi0  31692  atomli  32357  archirng  33152  archiabllem1a  33155  archiabllem2a  33158  archiabl  33162  crefi  33855  pcmplfin  33868  sigaclcu  34125  measvun  34217  signsply0  34559  bnj1128  34997  bnj1204  35019  bnj1417  35048  neibastop2lem  36393  poimirlem31  37690  ftc1cnnclem  37730  sdclem2  37781  heibor1lem  37848  cvrat4  39481  hdmapval2  41870  ismrcd1  42730  relexpxpmin  43749  ee222  44534  ee333  44539  ee1111  44548  sbcoreleleq  44567  ordelordALT  44569  trsbc  44572  ee110  44709  ee101  44711  ee011  44713  ee100  44715  ee010  44717  ee001  44719  eel11111  44754  fnchoice  45065  fiiuncl  45101  mullimc  45655  islptre  45658  mullimcf  45662  addlimc  45685  stoweidlem20  46057  stoweidlem59  46096  perfectALTVlem2  47752