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  8668  dffi3  8895  cantnflt  9135  cantnflem1  9152  axdc3lem2  9873  seqf1olem2  13411  wrd2ind  14085  relexpindlem  14422  rtrclind  14424  o1fsum  15168  lcmneg  15947  prmind2  16029  rami  16351  ramcl  16365  pslem  17816  telgsums  19113  islbs3  19927  mplsubglem  20214  mpllsslem  20215  psgndif  20746  gsummatr01lem4  21267  lmmo  21988  cnmpt12  22275  cnmpt22  22282  filss  22461  flimopn  22583  flimrest  22591  cfil3i  23872  equivcfil  23902  equivcau  23903  ovolicc2lem3  24120  limciun  24492  dvcnvrelem1  24614  dvfsumrlim  24628  dvfsum2  24631  dgrco  24865  scvxcvx  25563  ftalem3  25652  2sqlem6  25999  2sqlem8  26002  dchrisumlema  26064  dchrisumlem2  26066  gropd  26816  grstructd  26817  pthdepisspth  27516  pjoi0  29494  atomli  30159  archirng  30817  archiabllem1a  30820  archiabllem2a  30823  archiabl  30827  crefi  31111  pcmplfin  31124  sigaclcu  31376  measvun  31468  signsply0  31821  bnj1128  32262  bnj1204  32284  bnj1417  32313  noprefixmo  33202  neibastop2lem  33708  poimirlem31  34938  ftc1cnnclem  34980  sdclem2  35032  heibor1lem  35102  cvrat4  36594  hdmapval2  38983  ismrcd1  39315  relexpxpmin  40082  ee222  40856  ee333  40861  ee1111  40870  sbcoreleleq  40889  ordelordALT  40891  trsbc  40894  ee110  41031  ee101  41033  ee011  41035  ee100  41037  ee010  41039  ee001  41041  eel11111  41077  fnchoice  41306  fiiuncl  41347  mullimc  41917  islptre  41920  mullimcf  41924  addlimc  41949  stoweidlem20  42325  stoweidlem59  42364  perfectALTVlem2  43907