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  9175  dffi3  9450  cantnflt  9700  cantnflem1  9717  axdc3lem2  10556  seqf1olem2  14212  wrd2ind  14900  relexpindlem  15245  rtrclind  15247  o1fsum  16009  lcmneg  16807  prmind2  16889  rami  17222  ramcl  17236  pslem  18775  telgsums  20237  islbs3  21463  psgndif  21938  mplsubglem  22336  mpllsslem  22337  gsummatr01lem4  23003  lmmo  23728  cnmpt12  24016  cnmpt22  24023  filss  24202  flimopn  24324  flimrest  24332  cfil3i  25620  equivcfil  25650  equivcau  25651  ovolicc2lem3  25870  limciun  26244  dvcnvrelem1  26367  dvfsumrlim  26381  dvfsum2  26384  dgrco  26624  scvxcvx  27343  ftalem3  27432  2sqlem6  27780  2sqlem8  27783  dchrisumlema  27845  dchrisumlem2  27847  addsproplem1  28385  negsproplem1  28444  gropd  29639  grstructd  29640  pthdepisspth  30351  pjoi0  32349  atomli  33014  archirng  33819  archiabllem1a  33822  archiabllem2a  33825  archiabl  33829  crefi  34549  pcmplfin  34562  sigaclcu  34819  measvun  34912  signsply0  35250  bnj1128  35690  bnj1204  35712  bnj1417  35741  neibastop2lem  37326  poimirlem31  38761  ftc1cnnclem  38801  sdclem2  38868  heibor1lem  38935  cvrat4  40692  hdmapval2  43081  ismrcd1  43902  relexpxpmin  44909  ee222  45676  ee333  45681  ee1111  45690  sbcoreleleq  45709  ordelordALT  45711  trsbc  45714  ee110  45851  ee101  45853  ee011  45855  ee100  45857  ee010  45859  ee001  45861  eel11111  45896  fnchoice  46251  fiiuncl  46287  mullimc  46833  islptre  46836  mullimcf  46840  addlimc  46863  stoweidlem20  47235  stoweidlem59  47274  perfectALTVlem2  49025