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

Theorem syl5bbr 252
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 195 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 250 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  3bitr3g  280  biass  350  19.16  1767  19.19  1769  sbco2  1980  cbvab  2367  necon1bbid  2466  necon4abid  2476  elabgt  2848  sbceq1a  2931  sbcralt  2993  sbccsbg  3037  sbccsb2g  3038  disjxun  3918  iunpw  4461  ordunisuc2  4526  tfis  4536  tfinds  4541  dfom2  4549  xp11  5018  ressn  5117  fnssresb  5213  fun11iun  5350  dmfco  5445  dffo4  5528  f1ompt  5534  funressn  5558  fnsuppeq0  5585  elunirn  5629  fliftf  5666  resoprab2  5793  ralrnmpt2  5810  1stconst  6059  2ndconst  6060  opiota  6174  iinon  6243  dfsmo2  6250  oeeui  6486  omabs  6531  brecop  6637  ixpsnf1o  6742  boxcutc  6745  ac6sfi  6986  wemapwe  7284  sdom2en01  7812  ac6num  7990  zorn2lem7  8013  ttukeylem6  8025  alephval2  8074  fpwwe2  8145  fpwwe  8148  nqereu  8433  suplem2pr  8557  map2psrpr  8612  supsrlem  8613  fimaxre3  9583  infm3  9593  crne0  9619  nn1suc  9647  uzindOLD  9985  xmulneg1  10467  supxrbnd1  10518  supxrbnd2  10519  iccneg  10635  wrdind  11354  cnpart  11602  sqr00  11626  lo1resb  11915  o1resb  11917  absefib  12352  efieq1re  12353  sadadd2lem2  12515  saddisjlem  12529  prmind2  12643  mreacs  13404  issubc  13556  isfunc  13582  pospo  13951  eqgval  14501  resscntz  14642  frgpuplem  14916  0frgp  14923  divsabl  14992  dmdprd  15071  dprdcntz2  15108  dprd2d2  15114  isnzr2  15847  chrdvds  16314  chrcong  16315  znleval  16340  isphld  16390  isclo  16656  ist1-2  16907  isnrm2  16918  nconsubb  16981  subislly  17039  ptclsg  17141  qtopcld  17236  kqcldsat  17256  divstgplem  17635  tsmssubm  17657  caucfil  18541  ioorinv  18763  mbfss  18833  iblss2  18992  dvivthlem1  19187  lhop1  19193  mpfind  19260  pf1ind  19270  deg1leb  19313  reeff1o  19655  sincosq3sgn  19700  sincosq4sgn  19701  dcubic  19974  efrlim  20096  fsumharmonic  20137  isppw  20184  issqf  20206  fsumdvdsmul  20267  ppiub  20275  lgsdinn0  20411  h2hlm  21390  isch2  21633  ch0pss  21854  nmcfnlbi  22462  jplem1  22678  hatomistici  22772  mdsymlem5  22817  cdjreui  22842  subfacp1lem2a  22882  subfacp1lem6  22887  eupath2lem2  23073  ghomf1olem  23172  rtrclreclem.trans  23214  dfres3  23286  axlowdimlem14  23757  onsuct0  24054  elo  24206  prodeq3ii  24474  glmrngo  24648  bwt2  24758  lvsovso2  24793  supnuf  24795  supexr  24797  sdclem2  25618  fdc  25621  fdc1  25622  istotbnd3  25661  sstotbnd  25665  prdstotbnd  25684  rrncmslem  25722  diophin  26018  diophun  26019  diophrex  26021  3rexfrabdioph  26044  6rexfrabdioph  26046  7rexfrabdioph  26047  zindbi  26197  fveqsb  26823  bnj1468  27567  lub0N  28068  glb0N  28072  cdlemefrs29bpre0  29274  dvhb1dimN  29864  dvhopellsm  29996  dibord  30038  dochnel2  30271  mapdvalc  30508  mapdval4N  30511
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator