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  4652  nn0suc  4680  imainss  5096  xpexr2  5115  funeu2  5279  imadif  5327  fnop  5347  ssimaex  5584  suppss  5658  suppss2  6073  smores3  6370  tfrlem2  6392  tz7.48-2  6454  swoso  6691  isinf  7076  frfi  7102  dffi3  7184  marypha1lem  7186  ordtypelem7  7239  cantnfreslem  7377  cnfcom2lem  7404  r1pw  7517  rankxplim3  7551  dfac5  7755  cofsmo  7895  axcclem  8083  zorn2lem7  8129  wloglei  9305  divval  9426  uzind3  10105  uzind3OLD  10107  xrltnsym  10471  xaddf  10551  xrsupsslem  10625  xrinfmsslem  10626  0fz1  10813  hashunsng  11367  zsum  12191  sumss  12197  fsumss  12198  fsumcvg3  12202  abscvgcvg  12277  isumshft  12298  geoisum1  12335  geoisum1c  12336  mertenslem2  12341  rpnnen2lem5  12497  gcdcllem3  12692  eulerthlem2  12850  ramcl2lem  13056  imasvscafn  13439  mreexexlem4d  13549  mndcl  14372  cycsubgcl  14643  galactghm  14783  odlem2  14854  gexlem2  14893  mulgmhm  15127  mulgghm  15128  gsumval3  15191  gsumpt  15222  dprdfeq0  15257  rnglghm  15388  rngrghm  15389  lssssr  15710  lbsind  15833  mplmonmul  16208  mplcoe1  16209  mplcoe2  16211  cnsubrg  16432  elcls  16810  neips  16850  opnnei  16857  ordtbaslem  16918  ptclsg  17309  qtopeu  17407  comet  18059  metrest  18070  pcorevlem  18524  dyadmbl  18955  mbfeqalem  18997  i1fadd  19050  itg1addlem2  19052  itg2uba  19098  itgss  19166  dvcnp  19268  quotval  19672  vieta1lem2  19691  aalioulem3  19714  ulmdvlem3  19779  dvradcnv  19797  abelthlem6  19812  abelthlem9  19816  abelth  19817  logtayllem  20006  logtayl  20007  cxpcl  20021  recxpcl  20022  cxpcn3lem  20087  leibpi  20238  musum  20431  dchrelbas3  20477  sumdchr2  20509  lgscllem  20542  lgsdir2  20567  dchrvmasumiflem2  20651  rpvmasum2  20661  padicabv  20779  padicabvf  20780  padicabvcxp  20781  nmooval  21341  hiidge0  21677  hommval  22316  hfmmval  22319  nmcfnlbi  22632  mdslmd1i  22909  mdslmd3i  22912  sumdmdlem2  22999  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemi1  23061  ballotlemii  23062  xdivval  23102  suppss2f  23201  disjdifprg  23352  subfacp1lem5  23715  subfacp1lem6  23716  cvmliftlem10  23825  wfr3g  24255  tfr3ALT  24279  colinearperm1  24685  colinearperm5  24689  endofsegid  24708  segcon2  24728  seglecgr12im  24733  segletr  24737  colinbtwnle  24741  broutsideof2  24745  btwnoutside  24748  outsideoftr  24752  outsidele  24755  fordisxex  24954  unexun  25569  opnbnd  26243  heibor1lem  26533  heiborlem3  26537  heiborlem10  26544  ablo4pnp  26570  crngm4  26628  sdrgacs  27509  cntzsdrg  27510  lkrpssN  29353  pclvalN  30079  polvalN  30094  lclkrlem2x  31720  hgmaprnlem5N  32093
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