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  1981  cbvab  2374  necon1bbid  2473  necon4abid  2483  elabgt  2879  sbceq1a  2962  sbcralt  3024  sbccsbg  3070  sbccsb2g  3071  disjxun  3981  iunpw  4528  ordunisuc2  4593  tfis  4603  tfinds  4608  dfom2  4616  xp11  5085  ressn  5184  fnssresb  5280  fun11iun  5417  dmfco  5513  dffo4  5596  f1ompt  5602  funressn  5626  fnsuppeq0  5653  elunirn  5697  fliftf  5734  resoprab2  5861  ralrnmpt2  5878  1stconst  6127  2ndconst  6128  opiota  6242  iinon  6311  dfsmo2  6318  oeeui  6554  omabs  6599  brecop  6705  ixpsnf1o  6810  boxcutc  6813  ac6sfi  7055  wemapwe  7354  sdom2en01  7882  ac6num  8060  zorn2lem7  8083  ttukeylem6  8095  alephval2  8148  fpwwe2  8219  fpwwe  8222  nqereu  8507  suplem2pr  8631  map2psrpr  8686  supsrlem  8687  fimaxre3  9657  infm3  9667  crne0  9693  nn1suc  9721  uzindOLD  10059  xmulneg1  10541  supxrbnd1  10592  supxrbnd2  10593  iccneg  10709  wrdind  11428  cnpart  11676  sqr00  11700  lo1resb  11989  o1resb  11991  absefib  12426  efieq1re  12427  sadadd2lem2  12589  saddisjlem  12603  prmind2  12717  mreacs  13508  issubc  13660  isfunc  13686  pospo  14055  eqgval  14614  resscntz  14755  frgpuplem  15029  divsabl  15105  dmdprd  15184  dprdcntz2  15221  dprd2d2  15227  isnzr2  15963  chrdvds  16430  chrcong  16431  znleval  16456  isphld  16506  isclo  16772  ist1-2  17023  isnrm2  17034  nconsubb  17097  subislly  17155  ptclsg  17257  qtopcld  17352  kqcldsat  17372  divstgplem  17751  tsmssubm  17773  caucfil  18657  ioorinv  18879  mbfss  18949  iblss2  19108  dvivthlem1  19303  lhop1  19309  mpfind  19376  pf1ind  19386  deg1leb  19429  reeff1o  19771  sincosq3sgn  19816  sincosq4sgn  19817  dcubic  20090  efrlim  20212  fsumharmonic  20253  isppw  20300  issqf  20322  fsumdvdsmul  20383  ppiub  20391  lgsdinn0  20527  h2hlm  21506  isch2  21749  ch0pss  21970  nmcfnlbi  22578  jplem1  22794  hatomistici  22888  mdsymlem5  22933  cdjreui  22958  dfimafnf  22988  ballotlemsima  23021  subfacp1lem2a  23069  subfacp1lem6  23074  eupath2lem2  23260  ghomf1olem  23359  rtrclreclem.trans  23401  dfres3  23473  axlowdimlem14  23944  onsuct0  24241  elo  24393  prodeq3ii  24661  glmrngo  24835  bwt2  24945  lvsovso2  24980  supnuf  24982  supexr  24984  sdclem2  25805  fdc  25808  fdc1  25809  istotbnd3  25848  sstotbnd  25852  prdstotbnd  25871  rrncmslem  25909  diophin  26205  diophun  26206  diophrex  26208  3rexfrabdioph  26231  6rexfrabdioph  26233  7rexfrabdioph  26234  zindbi  26384  fveqsb  27010  stoweidlem35  27105  bnj1468  27911  lub0N  28530  glb0N  28534  cdlemefrs29bpre0  29736  dvhb1dimN  30326  dvhopellsm  30458  dibord  30500  dochnel2  30733  mapdvalc  30970  mapdval4N  30973
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