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

Theorem syl6rbbr 257
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 195 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 255 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  baib  873  reu8  3132  sbc6g  3188  r19.28z  3722  r19.28zv  3725  r19.37zv  3726  r19.45zv  3727  r19.27z  3728  r19.27zv  3729  r19.36zv  3730  ralidm  3733  ralsns  3846  rexsns  3847  ssunsn2  3960  iunconst  4103  iinconst  4104  ordsseleq  4612  reusv7OLD  4737  elpwun  4758  dfom2  4849  funssres  5495  fncnv  5517  fresaun  5616  dff1o5  5685  funimass4  5779  fndmdifeq0  5838  fneqeql2  5841  unpreima  5858  dffo3  5886  funfvima  5975  opabex3d  5991  opabex3  5992  f1eqcocnv  6030  fliftf  6039  isocnv3  6054  isomin  6059  f1oweALT  6076  eloprabga  6162  mpt22eqb  6181  fnwelem  6463  oe0m1  6767  oarec  6807  boxcutc  7107  ordunifi  7359  r1fin  7701  rankr1c  7749  iscard  7864  iscard2  7865  cardval2  7880  dfac3  8004  kmlem8  8039  infinf  8443  xrlenlt  9145  ltxrlt  9148  negcon2  9356  mulne0b  9665  dfinfmr  9987  crne0  9995  elznn  10299  zmax  10573  zq  10582  elfznelfzo  11194  sqrneglem  12074  rexanuz2  12155  sumsplit  12554  fsum2dlem  12556  fsumcom2  12560  odd2np1  12910  divalgb  12926  gcdcllem2  13014  mrcidb2  13845  lbsacsbs  16230  islpir2  16324  domnmuln0  16360  mplcoe1  16530  mplcoe2  16532  iscld4  17131  iscon2  17479  kgencn  17590  tx1cn  17643  tx2cn  17644  elmptrab  17861  isfbas  17863  fbfinnfr  17875  cnfcf  18076  fmucndlem  18323  prdsxmslem2  18561  blval2  18607  cnbl0  18810  cnblcld  18811  metcld  19260  ismbf  19524  ismbfcn  19525  itg1val2  19578  itg2split  19643  itg2monolem1  19644  aannenlem1  20247  pilem1  20369  sinq34lt0t  20419  ellogrn  20459  logeftb  20480  isusgra0  21378  constr3lem2  21635  ch0pss  22949  h1de2ctlem  23059  adjsym  23338  eigposi  23341  dfadj2  23390  elnlfn  23433  xppreima  24061  1stpreima  24097  2ndpreima  24098  1stmbfm  24612  2ndmbfm  24613  fprodcom2  25310  nofulllem1  25659  dffun10  25761  hfext  26126  cnambfre  26257  isfne4b  26352  neifg  26402  0totbnd  26484  fnnfpeq0  26741  isnacs2  26762  mrefg3  26764  pw2f1ocnv  27110  islinds2  27262  islbs4  27281  mamucl  27435  acsfn1p  27486  climreeq  27717  funressnfv  27970  bnj1454  29275  bnj984  29385  cvrval2  30134  cvrnbtwn2  30135  cvrnbtwn4  30139  hlateq  30258  islpln5  30394  islvol5  30438  pmap11  30621  4atex  30935  cdleme0ex2N  31083  cdlemefrs29pre00  31254  diaord  31907  dihmeetlem13N  32179  lcfl1  32352  lcfls1N  32395  mapdpglem3  32535
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 179
  Copyright terms: Public domain W3C validator