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

Theorem syl5bbr 251
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 194 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 249 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3bitr3g  279  biass  349  19.16  1879  19.19  1881  sbco2  2135  cbvab  2522  necon1bbid  2621  necon4abid  2631  elabgt  3039  sbceq1a  3131  sbcralt  3193  sbccsbg  3239  sbccsb2g  3240  disjxun  4170  iunpw  4718  ordunisuc2  4783  tfis  4793  tfinds  4798  dfom2  4806  xp11  5263  ressn  5367  fnssresb  5516  fun11iun  5654  dmfco  5756  dffo4  5844  f1ompt  5850  funressn  5878  fnsuppeq0  5912  elunirn  5957  fliftf  5996  resoprab2  6126  ralrnmpt2  6143  1stconst  6394  2ndconst  6395  opiota  6494  iinon  6561  dfsmo2  6568  oeeui  6804  omabs  6849  brecop  6956  ixpsnf1o  7061  boxcutc  7064  ac6sfi  7310  wemapwe  7610  sdom2en01  8138  ac6num  8315  zorn2lem7  8338  ttukeylem6  8350  alephval2  8403  fpwwe2  8474  fpwwe  8477  nqereu  8762  suplem2pr  8886  map2psrpr  8941  supsrlem  8942  fimaxre3  9913  infm3  9923  crne0  9949  nn1suc  9977  uzindOLD  10320  xmulneg1  10804  supxrbnd1  10856  supxrbnd2  10857  iccneg  10974  wrdind  11746  cnpart  12000  sqr00  12024  lo1resb  12313  o1resb  12315  absefib  12754  efieq1re  12755  sadadd2lem2  12917  saddisjlem  12931  prmind2  13045  mreacs  13838  issubc  13990  isfunc  14016  pospo  14385  eqgval  14944  resscntz  15085  frgpuplem  15359  divsabl  15435  dmdprd  15514  dprdcntz2  15551  dprd2d2  15557  isnzr2  16289  chrdvds  16764  chrcong  16765  znleval  16790  isphld  16840  isclo  17106  ist1-2  17365  isnrm2  17376  nconsubb  17439  subislly  17497  ptclsg  17600  qtopcld  17698  kqcldsat  17718  divstgplem  18103  tsmssubm  18125  ustuqtop  18229  utop2nei  18233  blval2  18558  caucfil  19189  ioorinv  19421  mbfss  19491  iblss2  19650  dvivthlem1  19845  lhop1  19851  mpfind  19918  pf1ind  19928  deg1leb  19971  reeff1o  20316  sincosq3sgn  20361  sincosq4sgn  20362  dcubic  20639  efrlim  20761  fsumharmonic  20803  isppw  20850  issqf  20872  fsumdvdsmul  20933  ppiub  20941  lgsdinn0  21077  eupath2lem2  21653  h2hlm  22436  isch2  22679  ch0pss  22900  nmcfnlbi  23508  jplem1  23724  hatomistici  23818  mdsymlem5  23863  cdjreui  23888  reuxfr4d  23930  dfimafnf  23996  funcnvmpt  24036  isarchi  24205  esumfsup  24413  esumpcvgval  24421  measvuni  24521  aean  24548  ballotlemsima  24726  subfacp1lem2a  24819  subfacp1lem6  24824  ghomf1olem  25058  rtrclreclem.trans  25099  dfres3  25330  eldm3  25333  axlowdimlem14  25798  onsuct0  26095  sdclem2  26336  fdc  26339  fdc1  26340  istotbnd3  26370  sstotbnd  26374  prdstotbnd  26393  rrncmslem  26431  diophin  26721  diophun  26722  diophrex  26724  3rexfrabdioph  26747  6rexfrabdioph  26749  7rexfrabdioph  26750  zindbi  26899  fveqsb  27523  stoweidlem35  27651  tz6.12-afv  27904  ndmaovg  27915  frgra2v  28103  bnj1468  28923  sbco2wAUX7  29288  sbco2OLD7  29436  lub0N  29672  glb0N  29676  cdlemefrs29bpre0  30878  dvhb1dimN  31468  dvhopellsm  31600  dibord  31642  dochnel2  31875  mapdvalc  32112  mapdval4N  32115
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 178
  Copyright terms: Public domain W3C validator