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  9059  dffi3  9337  cantnflt  9584  cantnflem1  9601  axdc3lem2  10364  seqf1olem2  13995  wrd2ind  14676  relexpindlem  15016  rtrclind  15018  o1fsum  15767  lcmneg  16563  prmind2  16645  rami  16977  ramcl  16991  pslem  18529  telgsums  19959  islbs3  21145  psgndif  21592  mplsubglem  21987  mpllsslem  21988  gsummatr01lem4  22633  lmmo  23355  cnmpt12  23642  cnmpt22  23649  filss  23828  flimopn  23950  flimrest  23958  cfil3i  25246  equivcfil  25276  equivcau  25277  ovolicc2lem3  25496  limciun  25871  dvcnvrelem1  25994  dvfsumrlim  26008  dvfsum2  26011  dgrco  26250  scvxcvx  26963  ftalem3  27052  2sqlem6  27400  2sqlem8  27403  dchrisumlema  27465  dchrisumlem2  27467  addsproplem1  27975  negsproplem1  28034  gropd  29114  grstructd  29115  pthdepisspth  29818  pjoi0  31803  atomli  32468  archirng  33264  archiabllem1a  33267  archiabllem2a  33270  archiabl  33274  crefi  34007  pcmplfin  34020  sigaclcu  34277  measvun  34369  signsply0  34711  bnj1128  35148  bnj1204  35170  bnj1417  35199  neibastop2lem  36558  poimirlem31  37986  ftc1cnnclem  38026  sdclem2  38077  heibor1lem  38144  cvrat4  39903  hdmapval2  42292  ismrcd1  43144  relexpxpmin  44162  ee222  44947  ee333  44952  ee1111  44961  sbcoreleleq  44980  ordelordALT  44982  trsbc  44985  ee110  45122  ee101  45124  ee011  45126  ee100  45128  ee010  45130  ee001  45132  eel11111  45167  fnchoice  45478  fiiuncl  45514  mullimc  46064  islptre  46067  mullimcf  46071  addlimc  46094  stoweidlem20  46466  stoweidlem59  46505  perfectALTVlem2  48210