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

Theorem syl5bbr 250
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bbr.1  |-  ( ps  <->  ph )
syl5bbr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5bbr  |-  ( ch 
->  ( ph  <->  th )
)

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3  |-  ( ps  <->  ph )
21bicomi 193 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 248 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitr3g  278  biass  348  19.16  1789  19.19  1791  sbco2  2028  cbvab  2403  necon1bbid  2502  necon4abid  2512  elabgt  2913  sbceq1a  3003  sbcralt  3065  sbccsbg  3111  sbccsb2g  3112  disjxun  4023  iunpw  4572  ordunisuc2  4637  tfis  4647  tfinds  4652  dfom2  4660  xp11  5113  ressn  5213  fnssresb  5358  fun11iun  5495  dmfco  5595  dffo4  5678  f1ompt  5684  funressn  5708  fnsuppeq0  5735  elunirn  5779  fliftf  5816  resoprab2  5943  ralrnmpt2  5960  1stconst  6209  2ndconst  6210  opiota  6292  iinon  6359  dfsmo2  6366  oeeui  6602  omabs  6647  brecop  6753  ixpsnf1o  6858  boxcutc  6861  ac6sfi  7103  wemapwe  7402  sdom2en01  7930  ac6num  8108  zorn2lem7  8131  ttukeylem6  8143  alephval2  8196  fpwwe2  8267  fpwwe  8270  nqereu  8555  suplem2pr  8679  map2psrpr  8734  supsrlem  8735  fimaxre3  9705  infm3  9715  crne0  9741  nn1suc  9769  uzindOLD  10108  xmulneg1  10591  supxrbnd1  10642  supxrbnd2  10643  iccneg  10759  wrdind  11479  cnpart  11727  sqr00  11751  lo1resb  12040  o1resb  12042  absefib  12480  efieq1re  12481  sadadd2lem2  12643  saddisjlem  12657  prmind2  12771  mreacs  13562  issubc  13714  isfunc  13740  pospo  14109  eqgval  14668  resscntz  14809  frgpuplem  15083  divsabl  15159  dmdprd  15238  dprdcntz2  15275  dprd2d2  15281  isnzr2  16017  chrdvds  16484  chrcong  16485  znleval  16510  isphld  16560  isclo  16826  ist1-2  17077  isnrm2  17088  nconsubb  17151  subislly  17209  ptclsg  17311  qtopcld  17406  kqcldsat  17426  divstgplem  17805  tsmssubm  17827  caucfil  18711  ioorinv  18933  mbfss  19003  iblss2  19162  dvivthlem1  19357  lhop1  19363  mpfind  19430  pf1ind  19440  deg1leb  19483  reeff1o  19825  sincosq3sgn  19870  sincosq4sgn  19871  dcubic  20144  efrlim  20266  fsumharmonic  20307  isppw  20354  issqf  20376  fsumdvdsmul  20437  ppiub  20445  lgsdinn0  20581  h2hlm  21562  isch2  21805  ch0pss  22026  nmcfnlbi  22634  jplem1  22850  hatomistici  22944  mdsymlem5  22989  cdjreui  23014  dfimafnf  23043  ballotlemsima  23076  reuxfr4d  23141  esumpcvgval  23448  subfacp1lem2a  23713  subfacp1lem6  23718  eupath2lem2  23904  ghomf1olem  24003  rtrclreclem.trans  24045  dfres3  24118  eldm3  24121  axlowdimlem14  24585  onsuct0  24882  elo  25052  prodeq3ii  25319  glmrngo  25493  bwt2  25603  lvsovso2  25638  supnuf  25640  supexr  25642  sdclem2  26463  fdc  26466  fdc1  26467  istotbnd3  26506  sstotbnd  26510  prdstotbnd  26529  rrncmslem  26567  diophin  26863  diophun  26864  diophrex  26866  3rexfrabdioph  26889  6rexfrabdioph  26891  7rexfrabdioph  26892  zindbi  27042  fveqsb  27667  stoweidlem35  27795  ndmaovg  28055  frgra2v  28188  bnj1468  28951  lub0N  29452  glb0N  29456  cdlemefrs29bpre0  30658  dvhb1dimN  31248  dvhopellsm  31380  dibord  31422  dochnel2  31655  mapdvalc  31892  mapdval4N  31895
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
  Copyright terms: Public domain W3C validator