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

Theorem syl6rbbr 255
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl6rbbr.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6rbbr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6rbbr  |-  ( ph  ->  ( th  <->  ps )
)

Proof of Theorem syl6rbbr
StepHypRef Expression
1 syl6rbbr.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6rbbr.2 . . 3  |-  ( th  <->  ch )
32bicomi 193 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 253 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  baib  871  reu8  2974  sbc6g  3029  r19.28z  3559  r19.28zv  3562  r19.37zv  3563  r19.45zv  3564  r19.27z  3565  r19.27zv  3566  r19.36zv  3567  ralidm  3570  ralsns  3683  rexsns  3684  ssunsn2  3789  iunconst  3929  iinconst  3930  ordsseleq  4437  reusv7OLD  4562  elpwun  4583  dfom2  4674  funssres  5310  fncnv  5330  fresaun  5428  dff1o5  5497  funimass4  5589  fndmdifeq0  5647  fneqeql2  5650  unpreima  5667  dffo3  5691  funfvima  5769  opabex3  5785  f1eqcocnv  5821  fliftf  5830  isocnv3  5845  isomin  5850  f1oweALT  5867  eloprabga  5950  mpt22eqb  5969  fnwelem  6246  oe0m1  6536  oarec  6576  boxcutc  6875  ordunifi  7123  r1fin  7461  rankr1c  7509  iscard  7624  iscard2  7625  cardval2  7640  dfac3  7764  kmlem8  7799  infinf  8204  xrlenlt  8906  ltxrlt  8909  negcon2  9116  mulne0b  9425  dfinfmr  9747  crne0  9755  elznn  10055  zmax  10329  zq  10338  sqrneglem  11768  rexanuz2  11849  sumsplit  12247  fsum2dlem  12249  fsumcom2  12253  odd2np1  12603  divalgb  12619  gcdcllem2  12707  mrcidb2  13536  lbsacsbs  15925  islpir2  16019  domnmuln0  16055  mplcoe1  16225  mplcoe2  16227  iscld4  16818  iscon2  17156  kgencn  17267  tx1cn  17319  tx2cn  17320  elmptrab  17538  isfbas  17540  fbfinnfr  17552  cnfcf  17753  prdsxmslem2  18091  cnbl0  18299  cnblcld  18300  metcld  18747  ismbf  19001  ismbfcn  19002  itg1val2  19055  itg2split  19120  itg2monolem1  19121  aannenlem1  19724  pilem1  19843  sinq34lt0t  19893  ellogrn  19933  logeftb  19953  ch0pss  22040  h1de2ctlem  22150  adjsym  22429  eigposi  22432  dfadj2  22481  elnlfn  22524  xppreima  23226  1stmbfm  23580  2ndmbfm  23581  nofulllem1  24427  hfext  24885  itgaddnclem2  25010  elo  25144  fopab2g  25248  fgsb2  25658  tcnvec  25793  cmppar3  26077  isfne4b  26373  neifg  26423  0totbnd  26600  fnnfpeq0  26861  isnacs2  26884  mrefg3  26886  pw2f1ocnv  27233  islinds2  27386  islbs4  27405  mamucl  27559  acsfn1p  27610  climreeq  27842  funressnfv  28096  opabex3d  28190  elfznelfzo  28213  isusgra0  28238  constr3lem2  28392  bnj1454  29190  bnj984  29300  cvrval2  30086  cvrnbtwn2  30087  cvrnbtwn4  30091  hlateq  30210  islpln5  30346  islvol5  30390  pmap11  30573  4atex  30887  cdleme0ex2N  31035  cdlemefrs29pre00  31206  diaord  31859  dihmeetlem13N  32131  lcfl1  32304  lcfls1N  32347  mapdpglem3  32487
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