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  9150  dffi3  9426  cantnflt  9676  cantnflem1  9693  axdc3lem2  10532  seqf1olem2  14188  wrd2ind  14876  relexpindlem  15221  rtrclind  15223  o1fsum  15985  lcmneg  16783  prmind2  16865  rami  17198  ramcl  17212  pslem  18751  telgsums  20212  islbs3  21438  psgndif  21913  mplsubglem  22311  mpllsslem  22312  gsummatr01lem4  22978  lmmo  23703  cnmpt12  23991  cnmpt22  23998  filss  24177  flimopn  24299  flimrest  24307  cfil3i  25595  equivcfil  25625  equivcau  25626  ovolicc2lem3  25845  limciun  26219  dvcnvrelem1  26342  dvfsumrlim  26356  dvfsum2  26359  dgrco  26599  scvxcvx  27318  ftalem3  27407  2sqlem6  27755  2sqlem8  27758  dchrisumlema  27820  dchrisumlem2  27822  addsproplem1  28360  negsproplem1  28419  gropd  29614  grstructd  29615  pthdepisspth  30326  pjoi0  32324  atomli  32989  archirng  33795  archiabllem1a  33798  archiabllem2a  33801  archiabl  33805  crefi  34525  pcmplfin  34538  sigaclcu  34795  measvun  34888  signsply0  35226  bnj1128  35666  bnj1204  35688  bnj1417  35717  neibastop2lem  37240  poimirlem31  38662  ftc1cnnclem  38702  sdclem2  38769  heibor1lem  38836  cvrat4  40593  hdmapval2  42982  ismrcd1  43802  relexpxpmin  44810  ee222  45578  ee333  45583  ee1111  45592  sbcoreleleq  45611  ordelordALT  45613  trsbc  45616  ee110  45753  ee101  45755  ee011  45757  ee100  45759  ee010  45761  ee001  45763  eel11111  45798  fnchoice  46139  fiiuncl  46175  mullimc  46721  islptre  46724  mullimcf  46728  addlimc  46751  stoweidlem20  47123  stoweidlem59  47162  perfectALTVlem2  48913