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

Theorem syl6rbbr 264
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 202 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 262 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  baib  896  reu8  3154  sbc6g  3211  r19.28z  3771  r19.28zv  3774  r19.37zv  3775  r19.45zv  3776  r19.27z  3777  r19.27zv  3778  r19.36zv  3779  ralidm  3782  ralsnsg  3908  rexsnsOLD  3910  eldifvsn  4005  ssunsn2  4031  iunconst  4178  iinconst  4179  reusv7OLD  4503  ordsseleq  4747  funssres  5457  fncnv  5481  fresaun  5581  dff1o5  5649  funimass4  5741  fndmdifeq0  5808  fneqeql2  5811  unpreima  5828  dffo3  5857  fnnfpeq0  5908  funfvima  5951  f1eqcocnv  5998  fliftf  6007  isocnv3  6022  isomin  6027  eloprabga  6176  mpt22eqb  6198  elpwun  6388  dfom2  6477  opabex3d  6554  opabex3  6555  f1oweALT  6560  fnwelem  6686  mptsuppd  6711  oe0m1  6960  oarec  7000  boxcutc  7305  ordunifi  7561  r1fin  7979  rankr1c  8027  iscard  8144  iscard2  8145  cardval2  8160  dfac3  8290  kmlem8  8325  infinf  8729  xrlenlt  9441  ltxrlt  9444  negcon2  9661  mulne0b  9976  dfinfmr  10306  crne0  10314  elznn  10661  zmax  10949  zq  10958  elfznelfzo  11629  hashneq0  12131  sqrneglem  12755  rexfiuz  12834  rexanuz2  12836  sumsplit  13234  fsum2dlem  13236  fsumcom2  13240  odd2np1  13591  divalgb  13607  gcdcllem2  13695  mrcidb2  14555  lbsacsbs  17236  islpir2  17332  domnmuln0  17369  mplcoe1  17543  mplcoe5  17547  mplcoe2OLD  17549  islinds2  18241  islbs4  18260  mamucl  18300  mavmulcl  18357  mdetunilem8  18424  iscld4  18668  iscon2  19017  kgencn  19128  tx1cn  19181  tx2cn  19182  elmptrab  19399  isfbas  19401  fbfinnfr  19413  cnfcf  19614  fmucndlem  19865  prdsxmslem2  20103  blval2  20149  cnbl0  20352  cnblcld  20353  metcld  20815  ismbf  21107  ismbfcn  21108  itg1val2  21161  itg2split  21226  itg2monolem1  21227  aannenlem1  21793  pilem1  21915  sinq34lt0t  21970  ellogrn  22010  logeftb  22031  ercgrg  22968  isusgra0  23274  constr3lem2  23531  ch0pss  24847  h1de2ctlem  24957  adjsym  25236  eigposi  25239  dfadj2  25288  elnlfn  25331  xppreima  25963  1stpreima  26000  2ndpreima  26001  prsdm  26343  prsrn  26344  1stmbfm  26674  2ndmbfm  26675  eulerpartlemn  26763  fprodcom2  27494  nofulllem1  27842  dffun10  27944  hfext  28220  cnambfre  28438  isfne4b  28540  neifg  28590  0totbnd  28670  isnacs2  29040  mrefg3  29042  pw2f1ocnv  29384  acsfn1p  29554  climreeq  29784  funressnfv  30032  sbcoreleleq  31239  bnj1454  31833  bnj984  31943  cvrval2  32917  cvrnbtwn2  32918  cvrnbtwn4  32922  hlateq  33041  islpln5  33177  islvol5  33221  pmap11  33404  4atex  33718  cdleme0ex2N  33866  cdlemefrs29pre00  34037  diaord  34690  dihmeetlem13N  34962  lcfl1  35135  lcfls1N  35178  mapdpglem3  35318  taupilem3  35610
  Copyright terms: Public domain W3C validator