MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl3c Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 syl3c.3 . 2 (𝜑𝜃)
2 syl3c.1 . . 3 (𝜑𝜓)
3 syl3c.2 . . 3 (𝜑𝜒)
4 syl3c.4 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
52, 3, 4sylc 65 . 2 (𝜑 → (𝜃𝜏))
61, 5mpd 15 1 (𝜑𝜏)
Colors of variables: wff setvar class
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  9006  dffi3  9301  cantnflt  9542  cantnflem1  9559  axdc3lem2  10321  seqf1olem2  13878  wrd2ind  14544  relexpindlem  14883  rtrclind  14885  o1fsum  15634  lcmneg  16415  prmind2  16497  rami  16823  ramcl  16837  pslem  18397  telgsums  19705  islbs3  20545  psgndif  20935  mplsubglem  21333  mpllsslem  21334  gsummatr01lem4  21935  lmmo  22659  cnmpt12  22946  cnmpt22  22953  filss  23132  flimopn  23254  flimrest  23262  cfil3i  24561  equivcfil  24591  equivcau  24592  ovolicc2lem3  24811  limciun  25186  dvcnvrelem1  25309  dvfsumrlim  25323  dvfsum2  25326  dgrco  25564  scvxcvx  26263  ftalem3  26352  2sqlem6  26699  2sqlem8  26702  dchrisumlema  26764  dchrisumlem2  26766  gropd  27787  grstructd  27788  pthdepisspth  28488  pjoi0  30464  atomli  31129  archirng  31825  archiabllem1a  31828  archiabllem2a  31831  archiabl  31835  crefi  32208  pcmplfin  32221  sigaclcu  32496  measvun  32588  signsply0  32943  bnj1128  33382  bnj1204  33404  bnj1417  33433  addsproplem1  34277  negsproplem1  34314  neibastop2lem  34763  poimirlem31  36040  ftc1cnnclem  36080  sdclem2  36132  heibor1lem  36199  cvrat4  37837  hdmapval2  40226  ismrcd1  40923  relexpxpmin  41788  ee222  42585  ee333  42590  ee1111  42599  sbcoreleleq  42618  ordelordALT  42620  trsbc  42623  ee110  42760  ee101  42762  ee011  42764  ee100  42766  ee010  42768  ee001  42770  eel11111  42806  fnchoice  43035  fiiuncl  43074  mullimc  43648  islptre  43651  mullimcf  43655  addlimc  43680  stoweidlem20  44052  stoweidlem59  44091  perfectALTVlem2  45705
  Copyright terms: Public domain W3C validator