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  9128  dffi3  9426  cantnflt  9667  cantnflem1  9684  axdc3lem2  10446  seqf1olem2  14008  wrd2ind  14673  relexpindlem  15010  rtrclind  15012  o1fsum  15759  lcmneg  16540  prmind2  16622  rami  16948  ramcl  16962  pslem  18525  telgsums  19861  islbs3  20768  psgndif  21155  mplsubglem  21558  mpllsslem  21559  gsummatr01lem4  22160  lmmo  22884  cnmpt12  23171  cnmpt22  23178  filss  23357  flimopn  23479  flimrest  23487  cfil3i  24786  equivcfil  24816  equivcau  24817  ovolicc2lem3  25036  limciun  25411  dvcnvrelem1  25534  dvfsumrlim  25548  dvfsum2  25551  dgrco  25789  scvxcvx  26490  ftalem3  26579  2sqlem6  26926  2sqlem8  26929  dchrisumlema  26991  dchrisumlem2  26993  addsproplem1  27453  negsproplem1  27502  gropd  28291  grstructd  28292  pthdepisspth  28992  pjoi0  30970  atomli  31635  archirng  32334  archiabllem1a  32337  archiabllem2a  32340  archiabl  32344  crefi  32827  pcmplfin  32840  sigaclcu  33115  measvun  33207  signsply0  33562  bnj1128  34001  bnj1204  34023  bnj1417  34052  neibastop2lem  35245  poimirlem31  36519  ftc1cnnclem  36559  sdclem2  36610  heibor1lem  36677  cvrat4  38314  hdmapval2  40703  ismrcd1  41436  relexpxpmin  42468  ee222  43263  ee333  43268  ee1111  43277  sbcoreleleq  43296  ordelordALT  43298  trsbc  43301  ee110  43438  ee101  43440  ee011  43442  ee100  43444  ee010  43446  ee001  43448  eel11111  43484  fnchoice  43713  fiiuncl  43752  mullimc  44332  islptre  44335  mullimcf  44339  addlimc  44364  stoweidlem20  44736  stoweidlem59  44775  perfectALTVlem2  46390