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

Theorem syl6rbbr 268
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 206 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 266 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  baib  912  cad1  1515  necon2abid  2679  reu8  3268  sbc6g  3326  r19.28z  3890  r19.28zv  3893  r19.37zv  3894  r19.45zv  3895  r19.44zv  3896  r19.27z  3897  r19.27zv  3898  r19.36zv  3899  ralidm  3902  ralsnsg  4029  rexsnsOLD  4031  eldifvsn  4130  ssunsn2  4157  iunconst  4306  iinconst  4307  ordsseleq  5469  funssres  5639  fncnv  5663  fresaun  5769  dff1o5  5838  funimass4  5930  fndmdifeq0  6001  fneqeql2  6004  unpreima  6019  dffo3  6050  fnnfpeq0  6108  funfvima  6153  f1eqcocnv  6212  fliftf  6221  isocnv3  6236  isomin  6241  eloprabga  6395  mpt22eqb  6417  elpwun  6616  dfom2  6706  opabex3d  6783  opabex3  6784  f1oweALT  6789  fnwelem  6920  mptsuppd  6947  dfrecs3  7097  oe0m1  7229  oarec  7269  boxcutc  7571  ordunifi  7825  r1fin  8247  rankr1c  8295  iscard  8412  iscard2  8413  cardval2  8428  dfac3  8554  kmlem8  8589  infinf  8993  xrlenlt  9701  ltxrlt  9706  negcon2  9929  mulne0b  10255  dfinfre  10590  dfinfmrOLD  10591  crne0  10604  elznn  10955  zmax  11263  zq  11272  elfznelfzo  12015  hashneq0  12546  xpcogend  13032  sqrtneglem  13324  rexfiuz  13404  rexanuz2  13406  sumsplit  13822  fsum2dlem  13824  fsumcom2  13828  fprodcom2  14031  odd2np1  14358  divalgb  14378  gcdcllem2  14467  mrcidb2  15517  fncnvimaeqv  15998  lbsacsbs  18372  islpir2  18468  domnmuln0  18515  mplcoe1  18682  mplcoe5  18685  islinds2  19363  islbs4  19382  mamucl  19418  mavmulcl  19564  mdetunilem8  19636  iscld4  20073  iscon2  20421  kgencn  20563  tx1cn  20616  tx2cn  20617  elmptrab  20834  isfbas  20836  fbfinnfr  20848  cnfcf  21049  fmucndlem  21298  prdsxmslem2  21536  blval2  21569  cnbl0  21786  cnblcld  21787  metcld  22267  ismbf  22578  ismbfcn  22579  itg1val2  22634  itg2split  22699  itg2monolem1  22700  aannenlem1  23276  pilem1  23398  sinq34lt0t  23456  ellogrn  23501  logeftb  23525  ercgrg  24554  isusgra0  25066  usgraop  25069  constr3lem2  25366  ch0pss  27090  h1de2ctlem  27200  adjsym  27478  eigposi  27481  dfadj2  27530  elnlfn  27573  xppreima  28244  1stpreima  28283  2ndpreima  28284  qtophaus  28665  prsdm  28722  prsrn  28723  1stmbfm  29084  2ndmbfm  29085  eulerpartlemn  29216  bnj1454  29655  bnj984  29765  nofulllem1  30590  dffun10  30680  hfext  30949  isfne4b  30996  neifg  31026  taupilem3  31678  topdifinfindis  31707  topdifinffinlem  31708  finxpsuclem  31747  poimirlem23  31921  poimirlem26  31924  cnambfre  31947  0totbnd  32063  cvrval2  32803  cvrnbtwn2  32804  cvrnbtwn4  32808  hlateq  32927  islpln5  33063  islvol5  33107  pmap11  33290  4atex  33604  cdleme0ex2N  33753  cdlemefrs29pre00  33925  diaord  34578  dihmeetlem13N  34850  lcfl1  35023  lcfls1N  35066  mapdpglem3  35206  isnacs2  35511  mrefg3  35513  pw2f1ocnv  35856  acsfn1p  36029  relexp0eq  36197  frege124d  36257  sbcoreleleq  36798  dffo3f  37344  climreeq  37557  funressnfv  38386  isusgr0  38916
  Copyright terms: Public domain W3C validator