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  9051  dffi3  9325  cantnflt  9572  cantnflem1  9589  axdc3lem2  10352  seqf1olem2  13959  wrd2ind  14640  relexpindlem  14980  rtrclind  14982  o1fsum  15730  lcmneg  16524  prmind2  16606  rami  16937  ramcl  16951  pslem  18488  telgsums  19915  islbs3  21102  psgndif  21549  mplsubglem  21946  mpllsslem  21947  gsummatr01lem4  22583  lmmo  23305  cnmpt12  23592  cnmpt22  23599  filss  23778  flimopn  23900  flimrest  23908  cfil3i  25206  equivcfil  25236  equivcau  25237  ovolicc2lem3  25457  limciun  25832  dvcnvrelem1  25959  dvfsumrlim  25975  dvfsum2  25978  dgrco  26218  scvxcvx  26933  ftalem3  27022  2sqlem6  27371  2sqlem8  27374  dchrisumlema  27436  dchrisumlem2  27438  addsproplem1  27922  negsproplem1  27980  gropd  29020  grstructd  29021  pthdepisspth  29724  pjoi0  31708  atomli  32373  archirng  33168  archiabllem1a  33171  archiabllem2a  33174  archiabl  33178  crefi  33871  pcmplfin  33884  sigaclcu  34141  measvun  34233  signsply0  34575  bnj1128  35013  bnj1204  35035  bnj1417  35064  neibastop2lem  36415  poimirlem31  37701  ftc1cnnclem  37741  sdclem2  37792  heibor1lem  37859  cvrat4  39552  hdmapval2  41941  ismrcd1  42805  relexpxpmin  43824  ee222  44609  ee333  44614  ee1111  44623  sbcoreleleq  44642  ordelordALT  44644  trsbc  44647  ee110  44784  ee101  44786  ee011  44788  ee100  44790  ee010  44792  ee001  44794  eel11111  44829  fnchoice  45140  fiiuncl  45176  mullimc  45730  islptre  45733  mullimcf  45737  addlimc  45760  stoweidlem20  46132  stoweidlem59  46171  perfectALTVlem2  47836