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

Theorem syl5bbr 263
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 206 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 261 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  3bitr3g  291  biass  361  19.16  2038  19.19  2040  sbcom2  2274  sbal2  2290  necon1bbid  2663  elabgt  3182  sbceq1a  3278  sbcralt  3340  sbccsb2  3794  disjxun  4400  xp11  5272  ressn  5372  fnssresb  5688  dmfco  5939  dffo4  6038  f1ompt  6044  funressn  6077  elunirnALT  6157  fliftf  6208  resoprab2  6393  elrnmpt2res  6410  ralrnmpt2  6411  iunpw  6605  ordunisuc2  6671  tfis  6681  tfinds  6686  dfom2  6694  fun11iun  6753  opiota  6852  1stconst  6884  2ndconst  6885  fnsuppeq0  6943  iinon  7059  dfsmo2  7066  oeeui  7303  omabs  7348  brecop  7456  ixpsnf1o  7562  boxcutc  7565  ac6sfi  7815  wemapwe  8202  sdom2en01  8732  ac6num  8909  zorn2lem7  8932  ttukeylem6  8944  alephval2  8997  fpwwe2  9068  fpwwe  9071  nqereu  9354  suplem2pr  9478  map2psrpr  9534  supsrlem  9535  fimaxre3  10553  infm3  10568  crne0  10602  nn1suc  10630  xmulneg1  11555  supxrbnd1  11607  supxrbnd2  11608  iccneg  11753  wrdmap  12698  wrdind  12833  rtrclreclem3  13123  cnpart  13303  sqrt00  13327  lo1resb  13628  o1resb  13630  absefib  14252  efieq1re  14253  sadadd2lem2  14424  saddisjlem  14438  prmind2  14635  mreacs  15564  issubc  15740  isfunc  15769  pospo  16219  mrcmndind  16613  eqgval  16866  resscntz  16985  frgpuplem  17422  qusabl  17503  dmdprd  17630  dprdcntz2  17671  dprd2d2  17677  isnzr2  18487  mpfind  18759  gsummoncoe1  18898  pf1ind  18943  chrdvds  19099  chrcong  19100  znleval  19125  isphld  19221  smadiadetr  19700  mp2pm2mplem4  19833  isclo  20103  ist1-2  20363  isnrm2  20374  bwth  20425  nconsubb  20438  subislly  20496  ptclsg  20630  qtopcld  20728  kqcldsat  20748  qustgplem  21135  tsmssubm  21157  ustuqtop  21261  utop2nei  21265  blval2  21577  caucfil  22253  ioorinv  22528  ioorinvOLD  22533  mbfss  22602  iblss2  22763  dvivthlem1  22960  lhop1  22966  deg1leb  23044  reeff1o  23402  sincosq3sgn  23455  sincosq4sgn  23456  dcubic  23772  efrlim  23895  fsumharmonic  23937  isppw  24041  issqf  24063  fsumdvdsmul  24124  ppiub  24132  lgsdinn0  24268  tglngne  24595  tgelrnln  24675  axlowdimlem14  24985  uhgraop  25031  eupath2lem2  25706  h2hlm  26633  isch2  26876  ch0pss  27098  nmcfnlbi  27705  jplem1  27921  hatomistici  28015  mdsymlem5  28060  cdjreui  28085  reuxfr4d  28126  dfimafnf  28233  funcnvmpt  28271  fpwrelmap  28318  nn0min  28384  isarchi  28499  ordtconlem1  28730  esumfsup  28891  esumpcvgval  28899  measvuni  29036  aean  29067  eulerpartlemgh  29211  ballotlemsima  29348  ballotlemsimaOLD  29386  sgn3da  29412  bnj1468  29657  subfacp1lem2a  29903  subfacp1lem6  29908  ghomf1olem  30312  dfres3  30399  eldm3  30402  onsuct0  31101  ptrest  31939  ptrecube  31940  poimirlem2  31942  poimirlem23  31963  sdclem2  32071  fdc  32074  fdc1  32075  istotbnd3  32103  sstotbnd  32107  prdstotbnd  32126  rrncmslem  32164  lub0N  32755  glb0N  32759  cdlemefrs29bpre0  33963  dvhb1dimN  34553  dvhopellsm  34685  dibord  34727  dochnel2  34960  mapdvalc  35197  mapdval4N  35200  diophin  35615  diophun  35616  diophrex  35618  3rexfrabdioph  35640  6rexfrabdioph  35642  7rexfrabdioph  35643  zindbi  35794  rababg  36179  relexpnul  36270  isprm7  36660  hashnzfzclim  36671  fveqsb  36806  cncfiooicclem1  37771  stoweidlem35  37896  tz6.12-afv  38675  ndmaovg  38686  nbgrssovtx  39432  isfusgracl  39791  isfusgraclALT  39793  usgfis  39811  usgfisALT  39815  aacllem  40593
  Copyright terms: Public domain W3C validator