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  9056  dffi3  9334  cantnflt  9581  cantnflem1  9598  axdc3lem2  10361  seqf1olem2  13965  wrd2ind  14646  relexpindlem  14986  rtrclind  14988  o1fsum  15736  lcmneg  16530  prmind2  16612  rami  16943  ramcl  16957  pslem  18495  telgsums  19922  islbs3  21110  psgndif  21557  mplsubglem  21954  mpllsslem  21955  gsummatr01lem4  22602  lmmo  23324  cnmpt12  23611  cnmpt22  23618  filss  23797  flimopn  23919  flimrest  23927  cfil3i  25225  equivcfil  25255  equivcau  25256  ovolicc2lem3  25476  limciun  25851  dvcnvrelem1  25978  dvfsumrlim  25994  dvfsum2  25997  dgrco  26237  scvxcvx  26952  ftalem3  27041  2sqlem6  27390  2sqlem8  27393  dchrisumlema  27455  dchrisumlem2  27457  addsproplem1  27965  negsproplem1  28024  gropd  29104  grstructd  29105  pthdepisspth  29808  pjoi0  31792  atomli  32457  archirng  33270  archiabllem1a  33273  archiabllem2a  33276  archiabl  33280  crefi  34004  pcmplfin  34017  sigaclcu  34274  measvun  34366  signsply0  34708  bnj1128  35146  bnj1204  35168  bnj1417  35197  neibastop2lem  36554  poimirlem31  37848  ftc1cnnclem  37888  sdclem2  37939  heibor1lem  38006  cvrat4  39699  hdmapval2  42088  ismrcd1  42936  relexpxpmin  43954  ee222  44739  ee333  44744  ee1111  44753  sbcoreleleq  44772  ordelordALT  44774  trsbc  44777  ee110  44914  ee101  44916  ee011  44918  ee100  44920  ee010  44922  ee001  44924  eel11111  44959  fnchoice  45270  fiiuncl  45306  mullimc  45858  islptre  45861  mullimcf  45865  addlimc  45888  stoweidlem20  46260  stoweidlem59  46299  perfectALTVlem2  47964