Theorem syl3c 67

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 66	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
6	1, 5	mpd 16	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  fodomr  9114  dffi3  9389  cantnflt  9639  cantnflem1  9656  axdc3lem2  10441  seqf1olem2  14085  wrd2ind  14767  relexpindlem  15107  rtrclind  15109  o1fsum  15872  lcmneg  16667  prmind2  16749  rami  17081  ramcl  17095  pslem  18634  telgsums  20069  islbs3  21290  psgndif  21763  mplsubglem  22159  mpllsslem  22160  gsummatr01lem4  22826  lmmo  23548  cnmpt12  23835  cnmpt22  23842  filss  24021  flimopn  24143  flimrest  24151  cfil3i  25439  equivcfil  25469  equivcau  25470  ovolicc2lem3  25689  limciun  26064  dvcnvrelem1  26187  dvfsumrlim  26201  dvfsum2  26204  dgrco  26443  scvxcvx  27161  ftalem3  27250  2sqlem6  27598  2sqlem8  27601  dchrisumlema  27663  dchrisumlem2  27665  addsproplem1  28173  negsproplem1  28232  gropd  29392  grstructd  29393  pthdepisspth  30095  pjoi0  32080  atomli  32745  archirng  33517  archiabllem1a  33520  archiabllem2a  33523  archiabl  33527  crefi  34246  pcmplfin  34259  sigaclcu  34516  measvun  34608  signsply0  34947  bnj1128  35387  bnj1204  35409  bnj1417  35438  neibastop2lem  36899  poimirlem31  38330  ftc1cnnclem  38370  sdclem2  38421  heibor1lem  38488  cvrat4  40245  hdmapval2  42634  ismrcd1  43457  relexpxpmin  44471  ee222  45239  ee333  45244  ee1111  45253  sbcoreleleq  45272  ordelordALT  45274  trsbc  45277  ee110  45414  ee101  45416  ee011  45418  ee100  45420  ee010  45422  ee001  45424  eel11111  45459  fnchoice  45777  fiiuncl  45813  mullimc  46360  islptre  46363  mullimcf  46367  addlimc  46390  stoweidlem20  46762  stoweidlem59  46801  perfectALTVlem2  48515