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  9052  dffi3  9340  cantnflt  9587  cantnflem1  9604  axdc3lem2  10364  seqf1olem2  13967  wrd2ind  14647  relexpindlem  14988  rtrclind  14990  o1fsum  15738  lcmneg  16532  prmind2  16614  rami  16945  ramcl  16959  pslem  18496  telgsums  19890  islbs3  21080  psgndif  21527  mplsubglem  21924  mpllsslem  21925  gsummatr01lem4  22561  lmmo  23283  cnmpt12  23570  cnmpt22  23577  filss  23756  flimopn  23878  flimrest  23886  cfil3i  25185  equivcfil  25215  equivcau  25216  ovolicc2lem3  25436  limciun  25811  dvcnvrelem1  25938  dvfsumrlim  25954  dvfsum2  25957  dgrco  26197  scvxcvx  26912  ftalem3  27001  2sqlem6  27350  2sqlem8  27353  dchrisumlema  27415  dchrisumlem2  27417  addsproplem1  27899  negsproplem1  27957  gropd  28994  grstructd  28995  pthdepisspth  29698  pjoi0  31679  atomli  32344  archirng  33140  archiabllem1a  33143  archiabllem2a  33146  archiabl  33150  crefi  33813  pcmplfin  33826  sigaclcu  34083  measvun  34175  signsply0  34518  bnj1128  34956  bnj1204  34978  bnj1417  35007  neibastop2lem  36333  poimirlem31  37630  ftc1cnnclem  37670  sdclem2  37721  heibor1lem  37788  cvrat4  39422  hdmapval2  41811  ismrcd1  42671  relexpxpmin  43690  ee222  44476  ee333  44481  ee1111  44490  sbcoreleleq  44509  ordelordALT  44511  trsbc  44514  ee110  44651  ee101  44653  ee011  44655  ee100  44657  ee010  44659  ee001  44661  eel11111  44696  fnchoice  45007  fiiuncl  45043  mullimc  45598  islptre  45601  mullimcf  45605  addlimc  45630  stoweidlem20  46002  stoweidlem59  46041  perfectALTVlem2  47707