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  1787  19.19  1789  sbco2  2026  cbvab  2401  necon1bbid  2500  necon4abid  2510  elabgt  2911  sbceq1a  3001  sbcralt  3063  sbccsbg  3109  sbccsb2g  3110  disjxun  4021  iunpw  4570  ordunisuc2  4635  tfis  4645  tfinds  4650  dfom2  4658  xp11  5111  ressn  5211  fnssresb  5356  fun11iun  5493  dmfco  5593  dffo4  5676  f1ompt  5682  funressn  5706  fnsuppeq0  5733  elunirn  5777  fliftf  5814  resoprab2  5941  ralrnmpt2  5958  1stconst  6207  2ndconst  6208  opiota  6290  iinon  6357  dfsmo2  6364  oeeui  6600  omabs  6645  brecop  6751  ixpsnf1o  6856  boxcutc  6859  ac6sfi  7101  wemapwe  7400  sdom2en01  7928  ac6num  8106  zorn2lem7  8129  ttukeylem6  8141  alephval2  8194  fpwwe2  8265  fpwwe  8268  nqereu  8553  suplem2pr  8677  map2psrpr  8732  supsrlem  8733  fimaxre3  9703  infm3  9713  crne0  9739  nn1suc  9767  uzindOLD  10106  xmulneg1  10589  supxrbnd1  10640  supxrbnd2  10641  iccneg  10757  wrdind  11477  cnpart  11725  sqr00  11749  lo1resb  12038  o1resb  12040  absefib  12478  efieq1re  12479  sadadd2lem2  12641  saddisjlem  12655  prmind2  12769  mreacs  13560  issubc  13712  isfunc  13738  pospo  14107  eqgval  14666  resscntz  14807  frgpuplem  15081  divsabl  15157  dmdprd  15236  dprdcntz2  15273  dprd2d2  15279  isnzr2  16015  chrdvds  16482  chrcong  16483  znleval  16508  isphld  16558  isclo  16824  ist1-2  17075  isnrm2  17086  nconsubb  17149  subislly  17207  ptclsg  17309  qtopcld  17404  kqcldsat  17424  divstgplem  17803  tsmssubm  17825  caucfil  18709  ioorinv  18931  mbfss  19001  iblss2  19160  dvivthlem1  19355  lhop1  19361  mpfind  19428  pf1ind  19438  deg1leb  19481  reeff1o  19823  sincosq3sgn  19868  sincosq4sgn  19869  dcubic  20142  efrlim  20264  fsumharmonic  20305  isppw  20352  issqf  20374  fsumdvdsmul  20435  ppiub  20443  lgsdinn0  20579  h2hlm  21560  isch2  21803  ch0pss  22024  nmcfnlbi  22632  jplem1  22848  hatomistici  22942  mdsymlem5  22987  cdjreui  23012  dfimafnf  23041  ballotlemsima  23074  reuxfr4d  23139  esumpcvgval  23446  subfacp1lem2a  23711  subfacp1lem6  23716  eupath2lem2  23902  ghomf1olem  24001  rtrclreclem.trans  24043  dfres3  24116  eldm3  24119  axlowdimlem14  24583  onsuct0  24880  elo  25041  prodeq3ii  25308  glmrngo  25482  bwt2  25592  lvsovso2  25627  supnuf  25629  supexr  25631  sdclem2  26452  fdc  26455  fdc1  26456  istotbnd3  26495  sstotbnd  26499  prdstotbnd  26518  rrncmslem  26556  diophin  26852  diophun  26853  diophrex  26855  3rexfrabdioph  26878  6rexfrabdioph  26880  7rexfrabdioph  26881  zindbi  27031  fveqsb  27656  stoweidlem35  27784  ndmaovg  28044  frgra2v  28177  bnj1468  28878  lub0N  29379  glb0N  29383  cdlemefrs29bpre0  30585  dvhb1dimN  31175  dvhopellsm  31307  dibord  31349  dochnel2  31582  mapdvalc  31819  mapdval4N  31822
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