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  9092  dffi3  9382  cantnflt  9625  cantnflem1  9642  axdc3lem2  10404  seqf1olem2  14007  wrd2ind  14688  relexpindlem  15029  rtrclind  15031  o1fsum  15779  lcmneg  16573  prmind2  16655  rami  16986  ramcl  17000  pslem  18531  telgsums  19923  islbs3  21065  psgndif  21511  mplsubglem  21908  mpllsslem  21909  gsummatr01lem4  22545  lmmo  23267  cnmpt12  23554  cnmpt22  23561  filss  23740  flimopn  23862  flimrest  23870  cfil3i  25169  equivcfil  25199  equivcau  25200  ovolicc2lem3  25420  limciun  25795  dvcnvrelem1  25922  dvfsumrlim  25938  dvfsum2  25941  dgrco  26181  scvxcvx  26896  ftalem3  26985  2sqlem6  27334  2sqlem8  27337  dchrisumlema  27399  dchrisumlem2  27401  addsproplem1  27876  negsproplem1  27934  gropd  28958  grstructd  28959  pthdepisspth  29665  pjoi0  31646  atomli  32311  archirng  33142  archiabllem1a  33145  archiabllem2a  33148  archiabl  33152  crefi  33837  pcmplfin  33850  sigaclcu  34107  measvun  34199  signsply0  34542  bnj1128  34980  bnj1204  35002  bnj1417  35031  neibastop2lem  36348  poimirlem31  37645  ftc1cnnclem  37685  sdclem2  37736  heibor1lem  37803  cvrat4  39437  hdmapval2  41826  ismrcd1  42686  relexpxpmin  43706  ee222  44492  ee333  44497  ee1111  44506  sbcoreleleq  44525  ordelordALT  44527  trsbc  44530  ee110  44667  ee101  44669  ee011  44671  ee100  44673  ee010  44675  ee001  44677  eel11111  44712  fnchoice  45023  fiiuncl  45059  mullimc  45614  islptre  45617  mullimcf  45621  addlimc  45646  stoweidlem20  46018  stoweidlem59  46057  perfectALTVlem2  47723