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

Theorem syl5bbr 267
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 207 . 2  |-  ( ph  <->  ps )
3 syl5bbr.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3syl5bb 265 1  |-  ( ch 
->  ( ph  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3bitr3g  295  biass  366  19.16  2057  19.19  2059  sbcom2  2294  sbal2  2310  necon1bbid  2682  elabgt  3170  sbceq1a  3266  sbcralt  3328  sbccsb2  3798  disjxun  4393  xp11  5278  ressn  5379  fnssresb  5698  dmfco  5954  dffo4  6053  f1ompt  6059  funressn  6093  elunirnALT  6175  fliftf  6226  resoprab2  6412  elrnmpt2res  6429  ralrnmpt2  6430  iunpw  6624  ordunisuc2  6690  tfis  6700  tfinds  6705  dfom2  6713  fun11iun  6772  opiota  6871  1stconst  6903  2ndconst  6904  fnsuppeq0  6962  iinon  7077  dfsmo2  7084  oeeui  7321  omabs  7366  brecop  7474  ixpsnf1o  7580  boxcutc  7583  ac6sfi  7833  wemapwe  8220  sdom2en01  8750  ac6num  8927  zorn2lem7  8950  ttukeylem6  8962  alephval2  9015  fpwwe2  9086  fpwwe  9089  nqereu  9372  suplem2pr  9496  map2psrpr  9552  supsrlem  9553  fimaxre3  10575  infm3  10590  crne0  10624  nn1suc  10652  xmulneg1  11580  supxrbnd1  11632  supxrbnd2  11633  iccneg  11779  wrdmap  12749  wrdind  12887  rtrclreclem3  13200  cnpart  13380  sqrt00  13404  lo1resb  13705  o1resb  13707  absefib  14329  efieq1re  14330  sadadd2lem2  14503  saddisjlem  14517  prmind2  14714  mreacs  15642  issubc  15818  isfunc  15847  pospo  16297  mrcmndind  16691  eqgval  16944  resscntz  17063  frgpuplem  17500  qusabl  17581  dmdprd  17708  dprdcntz2  17749  dprd2d2  17755  isnzr2  18564  mpfind  18836  gsummoncoe1  18975  pf1ind  19020  chrdvds  19176  chrcong  19177  znleval  19202  isphld  19298  smadiadetr  19777  mp2pm2mplem4  19910  isclo  20180  ist1-2  20440  isnrm2  20451  bwth  20502  nconsubb  20515  subislly  20573  ptclsg  20707  qtopcld  20805  kqcldsat  20825  qustgplem  21213  tsmssubm  21235  ustuqtop  21339  utop2nei  21343  blval2  21655  caucfil  22331  ioorinv  22607  ioorinvOLD  22612  mbfss  22681  iblss2  22842  dvivthlem1  23039  lhop1  23045  deg1leb  23123  reeff1o  23481  sincosq3sgn  23534  sincosq4sgn  23535  dcubic  23851  efrlim  23974  fsumharmonic  24016  isppw  24120  issqf  24142  fsumdvdsmul  24203  ppiub  24211  lgsdinn0  24347  tglngne  24674  tgelrnln  24754  axlowdimlem14  25064  uhgraop  25110  eupath2lem2  25785  h2hlm  26714  isch2  26957  ch0pss  27179  nmcfnlbi  27786  jplem1  28002  hatomistici  28096  mdsymlem5  28141  cdjreui  28166  reuxfr4d  28205  dfimafnf  28309  funcnvmpt  28346  fpwrelmap  28393  nn0min  28459  isarchi  28573  ordtconlem1  28804  esumfsup  28965  esumpcvgval  28973  measvuni  29110  aean  29140  eulerpartlemgh  29284  ballotlemsima  29421  ballotlemsimaOLD  29459  sgn3da  29485  bnj1468  29729  subfacp1lem2a  29975  subfacp1lem6  29980  ghomf1olem  30384  dfres3  30470  eldm3  30473  onsuct0  31172  ptrest  32003  ptrecube  32004  poimirlem2  32006  poimirlem23  32027  sdclem2  32135  fdc  32138  fdc1  32139  istotbnd3  32167  sstotbnd  32171  prdstotbnd  32190  rrncmslem  32228  lub0N  32826  glb0N  32830  cdlemefrs29bpre0  34034  dvhb1dimN  34624  dvhopellsm  34756  dibord  34798  dochnel2  35031  mapdvalc  35268  mapdval4N  35271  diophin  35686  diophun  35687  diophrex  35689  3rexfrabdioph  35711  6rexfrabdioph  35713  7rexfrabdioph  35714  zindbi  35865  rababg  36250  relexpnul  36341  isprm7  36730  hashnzfzclim  36741  fveqsb  36876  infxrbnd2  37679  cncfiooicclem1  37868  stoweidlem35  38008  tz6.12-afv  38820  ndmaovg  38831  nbgrssovtx  39596  eupth2lem2  40131  isfusgracl  40246  isfusgraclALT  40248  usgfis  40266  usgfisALT  40270  aacllem  41046
  Copyright terms: Public domain W3C validator