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  901  necon2abid  2695  reu8  3279  sbc6g  3337  r19.28z  3904  r19.28zv  3907  r19.37zv  3908  r19.45zv  3909  r19.27z  3910  r19.27zv  3911  r19.36zv  3912  ralidm  3915  ralsnsg  4043  rexsnsOLD  4045  eldifvsn  4144  ssunsn2  4171  iunconst  4321  iinconst  4322  reusv7OLD  4646  ordsseleq  4894  funssres  5615  fncnv  5639  fresaun  5743  dff1o5  5812  funimass4  5906  fndmdifeq0  5975  fneqeql2  5978  unpreima  5995  dffo3  6028  fnnfpeq0  6084  funfvima  6129  f1eqcocnv  6186  fliftf  6195  isocnv3  6210  isomin  6215  eloprabga  6371  mpt22eqb  6393  elpwun  6595  dfom2  6684  opabex3d  6760  opabex3  6761  f1oweALT  6766  fnwelem  6897  mptsuppd  6922  oe0m1  7170  oarec  7210  boxcutc  7511  ordunifi  7769  r1fin  8191  rankr1c  8239  iscard  8356  iscard2  8357  cardval2  8372  dfac3  8502  kmlem8  8537  infinf  8941  xrlenlt  9652  ltxrlt  9655  negcon2  9874  mulne0b  10193  dfinfmr  10523  crne0  10532  elznn  10883  zmax  11185  zq  11194  elfznelfzo  11891  hashneq0  12410  sqrtneglem  13076  rexfiuz  13156  rexanuz2  13158  sumsplit  13559  fsum2dlem  13561  fsumcom2  13565  odd2np1  13920  divalgb  13936  gcdcllem2  14024  mrcidb2  14889  lbsacsbs  17673  islpir2  17770  domnmuln0  17818  mplcoe1  17998  mplcoe5  18002  mplcoe2OLD  18004  islinds2  18718  islbs4  18737  mamucl  18773  mavmulcl  18919  mdetunilem8  18991  iscld4  19436  iscon2  19785  kgencn  19927  tx1cn  19980  tx2cn  19981  elmptrab  20198  isfbas  20200  fbfinnfr  20212  cnfcf  20413  fmucndlem  20664  prdsxmslem2  20902  blval2  20948  cnbl0  21151  cnblcld  21152  metcld  21614  ismbf  21907  ismbfcn  21908  itg1val2  21961  itg2split  22026  itg2monolem1  22027  aannenlem1  22593  pilem1  22715  sinq34lt0t  22771  ellogrn  22816  logeftb  22837  ercgrg  23777  isusgra0  24216  usgraop  24219  constr3lem2  24515  ch0pss  26232  h1de2ctlem  26342  adjsym  26621  eigposi  26624  dfadj2  26673  elnlfn  26716  xppreima  27356  1stpreima  27393  2ndpreima  27394  qtophaus  27709  prsdm  27766  prsrn  27767  1stmbfm  28101  2ndmbfm  28102  eulerpartlemn  28190  fprodcom2  29086  nofulllem1  29434  dffun10  29536  hfext  29812  cnambfre  30035  isfne4b  30131  neifg  30161  0totbnd  30241  isnacs2  30610  mrefg3  30612  pw2f1ocnv  30951  acsfn1p  31121  climreeq  31527  funressnfv  32051  fncnvimaeqv  32472  sbcoreleleq  33034  bnj1454  33628  bnj984  33738  cvrval2  34722  cvrnbtwn2  34723  cvrnbtwn4  34727  hlateq  34846  islpln5  34982  islvol5  35026  pmap11  35209  4atex  35523  cdleme0ex2N  35672  cdlemefrs29pre00  35844  diaord  36497  dihmeetlem13N  36769  lcfl1  36942  lcfls1N  36985  mapdpglem3  37125  taupilem3  37417  xpcogend  37449
  Copyright terms: Public domain W3C validator