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  2961  sbc6g  3016  r19.28z  3546  r19.28zv  3549  r19.37zv  3550  r19.45zv  3551  r19.27z  3552  r19.27zv  3553  r19.36zv  3554  ralidm  3557  ralsns  3670  rexsns  3671  ssunsn2  3773  iunconst  3913  iinconst  3914  ordsseleq  4421  reusv7OLD  4546  elpwun  4567  dfom2  4658  funssres  5294  fncnv  5314  fresaun  5412  dff1o5  5481  funimass4  5573  fndmdifeq0  5631  fneqeql2  5634  unpreima  5651  dffo3  5675  funfvima  5753  opabex3  5769  f1eqcocnv  5805  fliftf  5814  isocnv3  5829  isomin  5834  f1oweALT  5851  eloprabga  5934  mpt22eqb  5953  fnwelem  6230  oe0m1  6520  oarec  6560  boxcutc  6859  ordunifi  7107  r1fin  7445  rankr1c  7493  iscard  7608  iscard2  7609  cardval2  7624  dfac3  7748  kmlem8  7783  infinf  8188  xrlenlt  8890  ltxrlt  8893  negcon2  9100  mulne0b  9409  dfinfmr  9731  crne0  9739  elznn  10039  zmax  10313  zq  10322  sqrneglem  11752  rexanuz2  11833  sumsplit  12231  fsum2dlem  12233  fsumcom2  12237  odd2np1  12587  divalgb  12603  gcdcllem2  12691  mrcidb2  13520  lbsacsbs  15909  islpir2  16003  domnmuln0  16039  mplcoe1  16209  mplcoe2  16211  iscld4  16802  iscon2  17140  kgencn  17251  tx1cn  17303  tx2cn  17304  elmptrab  17522  isfbas  17524  fbfinnfr  17536  cnfcf  17737  prdsxmslem2  18075  cnbl0  18283  cnblcld  18284  metcld  18731  ismbf  18985  ismbfcn  18986  itg1val2  19039  itg2split  19104  itg2monolem1  19105  aannenlem1  19708  pilem1  19827  sinq34lt0t  19877  ellogrn  19917  logeftb  19937  ch0pss  22024  h1de2ctlem  22134  adjsym  22413  eigposi  22416  dfadj2  22465  elnlfn  22508  xppreima  23211  1stmbfm  23565  2ndmbfm  23566  nofulllem1  24356  hfext  24813  elo  25041  fopab2g  25145  fgsb2  25555  tcnvec  25690  cmppar3  25974  isfne4b  26270  neifg  26320  0totbnd  26497  fnnfpeq0  26758  isnacs2  26781  mrefg3  26783  pw2f1ocnv  27130  islinds2  27283  islbs4  27302  mamucl  27456  acsfn1p  27507  climreeq  27739  funressnfv  27991  isusgra0  28106  bnj1454  28874  bnj984  28984  cvrval2  29464  cvrnbtwn2  29465  cvrnbtwn4  29469  hlateq  29588  islpln5  29724  islvol5  29768  pmap11  29951  4atex  30265  cdleme0ex2N  30413  cdlemefrs29pre00  30584  diaord  31237  dihmeetlem13N  31509  lcfl1  31682  lcfls1N  31725  mapdpglem3  31865
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