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 ⊢ (𝜑 → 𝜏)

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  9117  dffi3  9392  cantnflt  9642  cantnflem1  9659  axdc3lem2  10436  seqf1olem2  14080  wrd2ind  14762  relexpindlem  15102  rtrclind  15104  o1fsum  15867  lcmneg  16662  prmind2  16744  rami  17076  ramcl  17090  pslem  18629  telgsums  20064  islbs3  21260  psgndif  21733  mplsubglem  22129  mpllsslem  22130  gsummatr01lem4  22796  lmmo  23518  cnmpt12  23805  cnmpt22  23812  filss  23991  flimopn  24113  flimrest  24121  cfil3i  25409  equivcfil  25439  equivcau  25440  ovolicc2lem3  25659  limciun  26034  dvcnvrelem1  26157  dvfsumrlim  26171  dvfsum2  26174  dgrco  26413  scvxcvx  27128  ftalem3  27217  2sqlem6  27565  2sqlem8  27568  dchrisumlema  27630  dchrisumlem2  27632  addsproplem1  28140  negsproplem1  28199  gropd  29359  grstructd  29360  pthdepisspth  30062  pjoi0  32047  atomli  32712  archirng  33486  archiabllem1a  33489  archiabllem2a  33492  archiabl  33496  crefi  34215  pcmplfin  34228  sigaclcu  34485  measvun  34577  signsply0  34916  bnj1128  35356  bnj1204  35378  bnj1417  35407  neibastop2lem  36849  poimirlem31  38280  ftc1cnnclem  38320  sdclem2  38371  heibor1lem  38438  cvrat4  40195  hdmapval2  42584  ismrcd1  43409  relexpxpmin  44423  ee222  45191  ee333  45196  ee1111  45205  sbcoreleleq  45224  ordelordALT  45226  trsbc  45229  ee110  45366  ee101  45368  ee011  45370  ee100  45372  ee010  45374  ee001  45376  eel11111  45411  fnchoice  45729  fiiuncl  45765  mullimc  46312  islptre  46315  mullimcf  46319  addlimc  46342  stoweidlem20  46714  stoweidlem59  46753  perfectALTVlem2  48464