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  9066  dffi3  9344  cantnflt  9593  cantnflem1  9610  axdc3lem2  10373  seqf1olem2  14004  wrd2ind  14685  relexpindlem  15025  rtrclind  15027  o1fsum  15776  lcmneg  16572  prmind2  16654  rami  16986  ramcl  17000  pslem  18538  telgsums  19968  islbs3  21153  psgndif  21582  mplsubglem  21977  mpllsslem  21978  gsummatr01lem4  22623  lmmo  23345  cnmpt12  23632  cnmpt22  23639  filss  23818  flimopn  23940  flimrest  23948  cfil3i  25236  equivcfil  25266  equivcau  25267  ovolicc2lem3  25486  limciun  25861  dvcnvrelem1  25984  dvfsumrlim  25998  dvfsum2  26001  dgrco  26240  scvxcvx  26949  ftalem3  27038  2sqlem6  27386  2sqlem8  27389  dchrisumlema  27451  dchrisumlem2  27453  addsproplem1  27961  negsproplem1  28020  gropd  29100  grstructd  29101  pthdepisspth  29803  pjoi0  31788  atomli  32453  archirng  33249  archiabllem1a  33252  archiabllem2a  33255  archiabl  33259  crefi  33991  pcmplfin  34004  sigaclcu  34261  measvun  34353  signsply0  34695  bnj1128  35132  bnj1204  35154  bnj1417  35183  neibastop2lem  36542  poimirlem31  37972  ftc1cnnclem  38012  sdclem2  38063  heibor1lem  38130  cvrat4  39889  hdmapval2  42278  ismrcd1  43130  relexpxpmin  44144  ee222  44929  ee333  44934  ee1111  44943  sbcoreleleq  44962  ordelordALT  44964  trsbc  44967  ee110  45104  ee101  45106  ee011  45108  ee100  45110  ee010  45112  ee001  45114  eel11111  45149  fnchoice  45460  fiiuncl  45496  mullimc  46046  islptre  46049  mullimcf  46053  addlimc  46076  stoweidlem20  46448  stoweidlem59  46487  perfectALTVlem2  48198