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  9130  dffi3  9405  cantnflt  9655  cantnflem1  9672  axdc3lem2  10457  seqf1olem2  14110  wrd2ind  14796  relexpindlem  15140  rtrclind  15142  o1fsum  15904  lcmneg  16699  prmind2  16781  rami  17113  ramcl  17127  pslem  18666  telgsums  20126  islbs3  21348  psgndif  21821  mplsubglem  22219  mpllsslem  22220  gsummatr01lem4  22886  lmmo  23611  cnmpt12  23899  cnmpt22  23906  filss  24085  flimopn  24207  flimrest  24215  cfil3i  25503  equivcfil  25533  equivcau  25534  ovolicc2lem3  25753  limciun  26128  dvcnvrelem1  26251  dvfsumrlim  26265  dvfsum2  26268  dgrco  26508  scvxcvx  27230  ftalem3  27319  2sqlem6  27667  2sqlem8  27670  dchrisumlema  27732  dchrisumlem2  27734  addsproplem1  28242  negsproplem1  28301  gropd  29496  grstructd  29497  pthdepisspth  30208  pjoi0  32206  atomli  32871  archirng  33636  archiabllem1a  33639  archiabllem2a  33642  archiabl  33646  crefi  34365  pcmplfin  34378  sigaclcu  34635  measvun  34728  signsply0  35067  bnj1128  35507  bnj1204  35529  bnj1417  35558  neibastop2lem  36987  poimirlem31  38408  ftc1cnnclem  38448  sdclem2  38500  heibor1lem  38567  cvrat4  40324  hdmapval2  42713  ismrcd1  43551  relexpxpmin  44565  ee222  45333  ee333  45338  ee1111  45347  sbcoreleleq  45366  ordelordALT  45368  trsbc  45371  ee110  45508  ee101  45510  ee011  45512  ee100  45514  ee010  45516  ee001  45518  eel11111  45553  fnchoice  45871  fiiuncl  45907  mullimc  46454  islptre  46457  mullimcf  46461  addlimc  46484  stoweidlem20  46856  stoweidlem59  46895  perfectALTVlem2  48646