MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan2br Unicode version

Theorem sylan2br 462
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2br.1  |-  ( ch  <->  ph )
sylan2br.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylan2br  |-  ( ( ps  /\  ph )  ->  th )

Proof of Theorem sylan2br
StepHypRef Expression
1 sylan2br.1 . . 3  |-  ( ch  <->  ph )
21biimpri 197 . 2  |-  ( ph  ->  ch )
3 sylan2br.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 460 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  syl2anbr  466  tfindsg2  4668  nn0suc  4696  imainss  5112  xpexr2  5131  funeu2  5295  imadif  5343  fnop  5363  ssimaex  5600  suppss  5674  suppss2  6089  smores3  6386  tfrlem2  6408  tz7.48-2  6470  swoso  6707  isinf  7092  frfi  7118  dffi3  7200  marypha1lem  7202  ordtypelem7  7255  cantnfreslem  7393  cnfcom2lem  7420  r1pw  7533  rankxplim3  7567  dfac5  7771  cofsmo  7911  axcclem  8099  zorn2lem7  8145  wloglei  9321  divval  9442  uzind3  10121  uzind3OLD  10123  xrltnsym  10487  xaddf  10567  xrsupsslem  10641  xrinfmsslem  10642  0fz1  10829  hashunsng  11383  zsum  12207  sumss  12213  fsumss  12214  fsumcvg3  12218  abscvgcvg  12293  isumshft  12314  geoisum1  12351  geoisum1c  12352  mertenslem2  12357  rpnnen2lem5  12513  gcdcllem3  12708  eulerthlem2  12866  ramcl2lem  13072  imasvscafn  13455  mreexexlem4d  13565  mndcl  14388  cycsubgcl  14659  galactghm  14799  odlem2  14870  gexlem2  14909  mulgmhm  15143  mulgghm  15144  gsumval3  15207  gsumpt  15238  dprdfeq0  15273  rnglghm  15404  rngrghm  15405  lssssr  15726  lbsind  15849  mplmonmul  16224  mplcoe1  16225  mplcoe2  16227  cnsubrg  16448  elcls  16826  neips  16866  opnnei  16873  ordtbaslem  16934  ptclsg  17325  qtopeu  17423  comet  18075  metrest  18086  pcorevlem  18540  dyadmbl  18971  mbfeqalem  19013  i1fadd  19066  itg1addlem2  19068  itg2uba  19114  itgss  19182  dvcnp  19284  quotval  19688  vieta1lem2  19707  aalioulem3  19730  ulmdvlem3  19795  dvradcnv  19813  abelthlem6  19828  abelthlem9  19832  abelth  19833  logtayllem  20022  logtayl  20023  cxpcl  20037  recxpcl  20038  cxpcn3lem  20103  leibpi  20254  musum  20447  dchrelbas3  20493  sumdchr2  20525  lgscllem  20558  lgsdir2  20583  dchrvmasumiflem2  20667  rpvmasum2  20677  padicabv  20795  padicabvf  20796  padicabvcxp  20797  nmooval  21357  hiidge0  21693  hommval  22332  hfmmval  22335  nmcfnlbi  22648  mdslmd1i  22925  mdslmd3i  22928  sumdmdlem2  23015  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemi1  23077  ballotlemii  23078  xdivval  23118  suppss2f  23216  disjdifprg  23367  subfacp1lem5  23730  subfacp1lem6  23731  cvmliftlem10  23840  zprod  24160  wfr3g  24326  tfr3ALT  24350  colinearperm1  24757  colinearperm5  24761  endofsegid  24780  segcon2  24800  seglecgr12im  24805  segletr  24809  colinbtwnle  24813  broutsideof2  24817  btwnoutside  24820  outsideoftr  24824  outsidele  24827  fordisxex  25057  unexun  25672  opnbnd  26346  heibor1lem  26636  heiborlem3  26640  heiborlem10  26647  ablo4pnp  26673  crngm4  26731  sdrgacs  27612  cntzsdrg  27613  lkrpssN  29975  pclvalN  30701  polvalN  30716  lclkrlem2x  32342  hgmaprnlem5N  32715
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator