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  9098  dffi3  9389  cantnflt  9632  cantnflem1  9649  axdc3lem2  10411  seqf1olem2  14014  wrd2ind  14695  relexpindlem  15036  rtrclind  15038  o1fsum  15786  lcmneg  16580  prmind2  16662  rami  16993  ramcl  17007  pslem  18538  telgsums  19930  islbs3  21072  psgndif  21518  mplsubglem  21915  mpllsslem  21916  gsummatr01lem4  22552  lmmo  23274  cnmpt12  23561  cnmpt22  23568  filss  23747  flimopn  23869  flimrest  23877  cfil3i  25176  equivcfil  25206  equivcau  25207  ovolicc2lem3  25427  limciun  25802  dvcnvrelem1  25929  dvfsumrlim  25945  dvfsum2  25948  dgrco  26188  scvxcvx  26903  ftalem3  26992  2sqlem6  27341  2sqlem8  27344  dchrisumlema  27406  dchrisumlem2  27408  addsproplem1  27883  negsproplem1  27941  gropd  28965  grstructd  28966  pthdepisspth  29672  pjoi0  31653  atomli  32318  archirng  33149  archiabllem1a  33152  archiabllem2a  33155  archiabl  33159  crefi  33844  pcmplfin  33857  sigaclcu  34114  measvun  34206  signsply0  34549  bnj1128  34987  bnj1204  35009  bnj1417  35038  neibastop2lem  36355  poimirlem31  37652  ftc1cnnclem  37692  sdclem2  37743  heibor1lem  37810  cvrat4  39444  hdmapval2  41833  ismrcd1  42693  relexpxpmin  43713  ee222  44499  ee333  44504  ee1111  44513  sbcoreleleq  44532  ordelordALT  44534  trsbc  44537  ee110  44674  ee101  44676  ee011  44678  ee100  44680  ee010  44682  ee001  44684  eel11111  44719  fnchoice  45030  fiiuncl  45066  mullimc  45621  islptre  45624  mullimcf  45628  addlimc  45653  stoweidlem20  46025  stoweidlem59  46064  perfectALTVlem2  47727