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  9166  dffi3  9468  cantnflt  9709  cantnflem1  9726  axdc3lem2  10488  seqf1olem2  14079  wrd2ind  14757  relexpindlem  15098  rtrclind  15100  o1fsum  15845  lcmneg  16636  prmind2  16718  rami  17048  ramcl  17062  pslem  18629  telgsums  20025  islbs3  21174  psgndif  21637  mplsubglem  22036  mpllsslem  22037  gsummatr01lem4  22679  lmmo  23403  cnmpt12  23690  cnmpt22  23697  filss  23876  flimopn  23998  flimrest  24006  cfil3i  25316  equivcfil  25346  equivcau  25347  ovolicc2lem3  25567  limciun  25943  dvcnvrelem1  26070  dvfsumrlim  26086  dvfsum2  26089  dgrco  26329  scvxcvx  27043  ftalem3  27132  2sqlem6  27481  2sqlem8  27484  dchrisumlema  27546  dchrisumlem2  27548  addsproplem1  28016  negsproplem1  28074  gropd  29062  grstructd  29063  pthdepisspth  29767  pjoi0  31745  atomli  32410  archirng  33177  archiabllem1a  33180  archiabllem2a  33183  archiabl  33187  crefi  33807  pcmplfin  33820  sigaclcu  34097  measvun  34189  signsply0  34544  bnj1128  34982  bnj1204  35004  bnj1417  35033  neibastop2lem  36342  poimirlem31  37637  ftc1cnnclem  37677  sdclem2  37728  heibor1lem  37795  cvrat4  39425  hdmapval2  41814  ismrcd1  42685  relexpxpmin  43706  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  44720  fnchoice  44966  fiiuncl  45004  mullimc  45571  islptre  45574  mullimcf  45578  addlimc  45603  stoweidlem20  45975  stoweidlem59  46014  perfectALTVlem2  47646