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

Theorem syl5bbr 262
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 205 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 260 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188
This theorem is referenced by:  3bitr3g  290  biass  360  19.16  2012  19.19  2014  sbcom2  2238  sbal2  2254  cbvabOLD  2562  necon1bbid  2672  necon4abidOLD  2674  elabgt  3212  sbceq1a  3307  sbcralt  3369  sbccsb2  3819  disjxun  4415  xp11  5283  ressn  5383  fnssresb  5697  dmfco  5946  dffo4  6044  f1ompt  6050  funressn  6083  elunirnALT  6163  fliftf  6214  resoprab2  6398  elrnmpt2res  6415  ralrnmpt2  6416  iunpw  6610  ordunisuc2  6676  tfis  6686  tfinds  6691  dfom2  6699  fun11iun  6758  opiota  6857  1stconst  6886  2ndconst  6887  fnsuppeq0  6945  iinon  7058  dfsmo2  7065  oeeui  7302  omabs  7347  brecop  7455  ixpsnf1o  7561  boxcutc  7564  ac6sfi  7812  wemapwe  8192  sdom2en01  8721  ac6num  8898  zorn2lem7  8921  ttukeylem6  8933  alephval2  8986  fpwwe2  9057  fpwwe  9060  nqereu  9343  suplem2pr  9467  map2psrpr  9523  supsrlem  9524  fimaxre3  10542  infm3  10557  crne0  10591  nn1suc  10619  xmulneg1  11544  supxrbnd1  11596  supxrbnd2  11597  iccneg  11740  wrdmap  12674  wrdind  12807  rtrclreclem3  13091  cnpart  13271  sqrt00  13295  lo1resb  13595  o1resb  13597  absefib  14219  efieq1re  14220  sadadd2lem2  14387  saddisjlem  14401  prmind2  14595  mreacs  15508  issubc  15684  isfunc  15713  pospo  16163  mrcmndind  16557  eqgval  16810  resscntz  16929  frgpuplem  17350  qusabl  17431  dmdprd  17558  dprdcntz2  17599  dprd2d2  17605  isnzr2  18415  mpfind  18687  gsummoncoe1  18826  pf1ind  18871  chrdvds  19023  chrcong  19024  znleval  19049  isphld  19145  smadiadetr  19624  mp2pm2mplem4  19757  isclo  20027  ist1-2  20287  isnrm2  20298  bwth  20349  nconsubb  20362  subislly  20420  ptclsg  20554  qtopcld  20652  kqcldsat  20672  qustgplem  21059  tsmssubm  21081  ustuqtop  21185  utop2nei  21189  blval2  21501  caucfil  22139  ioorinv  22402  ioorinvOLD  22407  mbfss  22476  iblss2  22637  dvivthlem1  22834  lhop1  22840  deg1leb  22918  reeff1o  23264  sincosq3sgn  23317  sincosq4sgn  23318  dcubic  23634  efrlim  23757  fsumharmonic  23799  isppw  23901  issqf  23923  fsumdvdsmul  23984  ppiub  23992  lgsdinn0  24128  tglngne  24452  tgelrnln  24531  axlowdimlem14  24828  uhgraop  24874  eupath2lem2  25548  h2hlm  26465  isch2  26708  ch0pss  26930  nmcfnlbi  27537  jplem1  27753  hatomistici  27847  mdsymlem5  27892  cdjreui  27917  reuxfr4d  27958  dfimafnf  28070  funcnvmpt  28108  fpwrelmap  28158  nn0min  28219  isarchi  28334  ordtconlem1  28566  esumfsup  28727  esumpcvgval  28735  measvuni  28872  aean  28903  eulerpartlemgh  29034  ballotlemsima  29171  sgn3da  29197  bnj1468  29442  subfacp1lem2a  29688  subfacp1lem6  29693  ghomf1olem  30097  dfres3  30183  eldm3  30186  onsuct0  30883  ptrest  31643  ptrecube  31644  poimirlem2  31646  poimirlem23  31667  sdclem2  31775  fdc  31778  fdc1  31779  istotbnd3  31807  sstotbnd  31811  prdstotbnd  31830  rrncmslem  31868  lub0N  32464  glb0N  32468  cdlemefrs29bpre0  33672  dvhb1dimN  34262  dvhopellsm  34394  dibord  34436  dochnel2  34669  mapdvalc  34906  mapdval4N  34909  diophin  35324  diophun  35325  diophrex  35327  3rexfrabdioph  35349  6rexfrabdioph  35351  7rexfrabdioph  35352  zindbi  35504  relexpnul  35913  isprm7  36301  hashnzfzclim  36312  fveqsb  36447  cncfiooicclem1  37347  stoweidlem35  37469  tz6.12-afv  38078  ndmaovg  38089  isfusgracl  38509  isfusgraclALT  38511  usgfis  38529  usgfisALT  38533  aacllem  39314
  Copyright terms: Public domain W3C validator