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  1799  19.19  1801  sbco2  2039  cbvab  2414  necon1bbid  2513  necon4abid  2523  elabgt  2924  sbceq1a  3014  sbcralt  3076  sbccsbg  3122  sbccsb2g  3123  disjxun  4037  iunpw  4586  ordunisuc2  4651  tfis  4661  tfinds  4666  dfom2  4674  xp11  5127  ressn  5227  fnssresb  5372  fun11iun  5509  dmfco  5609  dffo4  5692  f1ompt  5698  funressn  5722  fnsuppeq0  5749  elunirn  5793  fliftf  5830  resoprab2  5957  ralrnmpt2  5974  1stconst  6223  2ndconst  6224  opiota  6306  iinon  6373  dfsmo2  6380  oeeui  6616  omabs  6661  brecop  6767  ixpsnf1o  6872  boxcutc  6875  ac6sfi  7117  wemapwe  7416  sdom2en01  7944  ac6num  8122  zorn2lem7  8145  ttukeylem6  8157  alephval2  8210  fpwwe2  8281  fpwwe  8284  nqereu  8569  suplem2pr  8693  map2psrpr  8748  supsrlem  8749  fimaxre3  9719  infm3  9729  crne0  9755  nn1suc  9783  uzindOLD  10122  xmulneg1  10605  supxrbnd1  10656  supxrbnd2  10657  iccneg  10773  wrdind  11493  cnpart  11741  sqr00  11765  lo1resb  12054  o1resb  12056  absefib  12494  efieq1re  12495  sadadd2lem2  12657  saddisjlem  12671  prmind2  12785  mreacs  13576  issubc  13728  isfunc  13754  pospo  14123  eqgval  14682  resscntz  14823  frgpuplem  15097  divsabl  15173  dmdprd  15252  dprdcntz2  15289  dprd2d2  15295  isnzr2  16031  chrdvds  16498  chrcong  16499  znleval  16524  isphld  16574  isclo  16840  ist1-2  17091  isnrm2  17102  nconsubb  17165  subislly  17223  ptclsg  17325  qtopcld  17420  kqcldsat  17440  divstgplem  17819  tsmssubm  17841  caucfil  18725  ioorinv  18947  mbfss  19017  iblss2  19176  dvivthlem1  19371  lhop1  19377  mpfind  19444  pf1ind  19454  deg1leb  19497  reeff1o  19839  sincosq3sgn  19884  sincosq4sgn  19885  dcubic  20158  efrlim  20280  fsumharmonic  20321  isppw  20368  issqf  20390  fsumdvdsmul  20451  ppiub  20459  lgsdinn0  20595  h2hlm  21576  isch2  21819  ch0pss  22040  nmcfnlbi  22648  jplem1  22864  hatomistici  22958  mdsymlem5  23003  cdjreui  23028  dfimafnf  23057  ballotlemsima  23090  reuxfr4d  23155  esumpcvgval  23461  subfacp1lem2a  23726  subfacp1lem6  23731  eupath2lem2  23917  ghomf1olem  24016  rtrclreclem.trans  24058  dfres3  24187  eldm3  24190  axlowdimlem14  24655  onsuct0  24952  elo  25144  prodeq3ii  25411  glmrngo  25585  bwt2  25695  lvsovso2  25730  supnuf  25732  supexr  25734  sdclem2  26555  fdc  26558  fdc1  26559  istotbnd3  26598  sstotbnd  26602  prdstotbnd  26621  rrncmslem  26659  diophin  26955  diophun  26956  diophrex  26958  3rexfrabdioph  26981  6rexfrabdioph  26983  7rexfrabdioph  26984  zindbi  27134  fveqsb  27759  stoweidlem35  27887  tz6.12-afv  28141  ndmaovg  28152  frgra2v  28423  bnj1468  29194  sbco2wAUX7  29559  sbco2OLD7  29706  lub0N  30001  glb0N  30005  cdlemefrs29bpre0  31207  dvhb1dimN  31797  dvhopellsm  31929  dibord  31971  dochnel2  32204  mapdvalc  32441  mapdval4N  32444
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