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  9048  dffi3  9322  cantnflt  9569  cantnflem1  9586  axdc3lem2  10349  seqf1olem2  13951  wrd2ind  14632  relexpindlem  14972  rtrclind  14974  o1fsum  15722  lcmneg  16516  prmind2  16598  rami  16929  ramcl  16943  pslem  18480  telgsums  19907  islbs3  21094  psgndif  21541  mplsubglem  21937  mpllsslem  21938  gsummatr01lem4  22574  lmmo  23296  cnmpt12  23583  cnmpt22  23590  filss  23769  flimopn  23891  flimrest  23899  cfil3i  25197  equivcfil  25227  equivcau  25228  ovolicc2lem3  25448  limciun  25823  dvcnvrelem1  25950  dvfsumrlim  25966  dvfsum2  25969  dgrco  26209  scvxcvx  26924  ftalem3  27013  2sqlem6  27362  2sqlem8  27365  dchrisumlema  27427  dchrisumlem2  27429  addsproplem1  27913  negsproplem1  27971  gropd  29011  grstructd  29012  pthdepisspth  29715  pjoi0  31699  atomli  32364  archirng  33164  archiabllem1a  33167  archiabllem2a  33170  archiabl  33174  crefi  33881  pcmplfin  33894  sigaclcu  34151  measvun  34243  signsply0  34585  bnj1128  35023  bnj1204  35045  bnj1417  35074  neibastop2lem  36425  poimirlem31  37711  ftc1cnnclem  37751  sdclem2  37802  heibor1lem  37869  cvrat4  39562  hdmapval2  41951  ismrcd1  42815  relexpxpmin  43834  ee222  44619  ee333  44624  ee1111  44633  sbcoreleleq  44652  ordelordALT  44654  trsbc  44657  ee110  44794  ee101  44796  ee011  44798  ee100  44800  ee010  44802  ee001  44804  eel11111  44839  fnchoice  45150  fiiuncl  45186  mullimc  45740  islptre  45743  mullimcf  45747  addlimc  45770  stoweidlem20  46142  stoweidlem59  46181  perfectALTVlem2  47846