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

Theorem sylan2br 463
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 198 . 2  |-  ( ph  ->  ch )
3 sylan2br.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan2 461 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  syl2anbr  467  tfindsg2  4833  nn0suc  4861  imainss  5279  xpexr2  5300  funeu2  5470  imadif  5520  fnop  5540  ssimaex  5780  suppss  5855  suppss2  6292  smores3  6607  tfrlem2  6629  tz7.48-2  6691  swoso  6928  isinf  7314  frfi  7344  dffi3  7428  marypha1lem  7430  ordtypelem7  7485  cantnfreslem  7623  cnfcom2lem  7650  r1pw  7763  rankxplim3  7797  dfac5  8001  cofsmo  8141  axcclem  8329  zorn2lem7  8374  wloglei  9551  divval  9672  uzind3  10355  uzind3OLD  10357  xrltnsym  10722  xaddf  10802  xrsupsslem  10877  xrinfmsslem  10878  0fz1  11066  hashunsng  11657  hashgt0elexb  11663  zsum  12504  sumss  12510  fsumss  12511  fsumcvg3  12515  abscvgcvg  12590  isumshft  12611  geoisum1  12648  geoisum1c  12649  mertenslem2  12654  rpnnen2lem5  12810  gcdcllem3  13005  eulerthlem2  13163  ramcl2lem  13369  imasvscafn  13754  mreexexlem4d  13864  mndcl  14687  cycsubgcl  14958  galactghm  15098  odlem2  15169  gexlem2  15208  mulgmhm  15442  mulgghm  15443  gsumval3  15506  gsumpt  15537  dprdfeq0  15572  rnglghm  15703  rngrghm  15704  lssssr  16021  lbsind  16144  mplmonmul  16519  mplcoe1  16520  mplcoe2  16522  cnsubrg  16751  elcls  17129  neips  17169  opnnei  17176  ordtbaslem  17244  ptclsg  17639  qtopeu  17740  xmetpsmet  18370  comet  18535  metrest  18546  pcorevlem  19043  dyadmbl  19484  mbfeqalem  19526  i1fadd  19579  itg1addlem2  19581  itg2uba  19627  itgss  19695  dvcnp  19797  quotval  20201  vieta1lem2  20220  aalioulem3  20243  ulmdvlem3  20310  dvradcnv  20329  abelthlem6  20344  abelthlem9  20348  abelth  20349  logtayllem  20542  logtayl  20543  cxpcl  20557  recxpcl  20558  cxpcn3lem  20623  leibpi  20774  musum  20968  dchrelbas3  21014  sumdchr2  21046  lgscllem  21079  lgsdir2  21104  dchrvmasumiflem2  21188  rpvmasum2  21198  padicabv  21316  padicabvf  21317  padicabvcxp  21318  nmooval  22256  hiidge0  22592  hommval  23231  hfmmval  23234  nmcfnlbi  23547  mdslmd1i  23824  mdslmd3i  23827  sumdmdlem2  23914  disjdifprg  24009  suppss2f  24041  xdivval  24157  esumfsupre  24453  dya2iocnei  24624  ballotlemfc0  24742  ballotlemfcc  24743  subfacp1lem5  24862  subfacp1lem6  24863  cvmliftlem10  24973  zprod  25255  prodss  25265  fprodss  25266  wfr3g  25529  tfr3ALT  25552  colinearperm1  25988  colinearperm5  25992  endofsegid  26011  segcon2  26031  seglecgr12im  26036  segletr  26040  colinbtwnle  26044  broutsideof2  26048  btwnoutside  26051  outsideoftr  26055  outsidele  26058  opnbnd  26319  heibor1lem  26509  heiborlem3  26513  heiborlem10  26520  ablo4pnp  26546  crngm4  26604  sdrgacs  27477  cntzsdrg  27478  lkrpssN  29898  pclvalN  30624  polvalN  30639  lclkrlem2x  32265  hgmaprnlem5N  32638
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 178  df-an 361
  Copyright terms: Public domain W3C validator