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  9142  dffi3  9443  cantnflt  9686  cantnflem1  9703  axdc3lem2  10465  seqf1olem2  14060  wrd2ind  14741  relexpindlem  15082  rtrclind  15084  o1fsum  15829  lcmneg  16622  prmind2  16704  rami  17035  ramcl  17049  pslem  18582  telgsums  19974  islbs3  21116  psgndif  21562  mplsubglem  21959  mpllsslem  21960  gsummatr01lem4  22596  lmmo  23318  cnmpt12  23605  cnmpt22  23612  filss  23791  flimopn  23913  flimrest  23921  cfil3i  25221  equivcfil  25251  equivcau  25252  ovolicc2lem3  25472  limciun  25847  dvcnvrelem1  25974  dvfsumrlim  25990  dvfsum2  25993  dgrco  26233  scvxcvx  26948  ftalem3  27037  2sqlem6  27386  2sqlem8  27389  dchrisumlema  27451  dchrisumlem2  27453  addsproplem1  27928  negsproplem1  27986  gropd  29010  grstructd  29011  pthdepisspth  29717  pjoi0  31698  atomli  32363  archirng  33186  archiabllem1a  33189  archiabllem2a  33192  archiabl  33196  crefi  33878  pcmplfin  33891  sigaclcu  34148  measvun  34240  signsply0  34583  bnj1128  35021  bnj1204  35043  bnj1417  35072  neibastop2lem  36378  poimirlem31  37675  ftc1cnnclem  37715  sdclem2  37766  heibor1lem  37833  cvrat4  39462  hdmapval2  41851  ismrcd1  42721  relexpxpmin  43741  ee222  44527  ee333  44532  ee1111  44541  sbcoreleleq  44560  ordelordALT  44562  trsbc  44565  ee110  44702  ee101  44704  ee011  44706  ee100  44708  ee010  44710  ee001  44712  eel11111  44747  fnchoice  45053  fiiuncl  45089  mullimc  45645  islptre  45648  mullimcf  45652  addlimc  45677  stoweidlem20  46049  stoweidlem59  46088  perfectALTVlem2  47736