MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6rbbr Structured version   Visualization 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  914  cad1  1519  necon2abid  2666  reu8  3234  sbc6g  3293  r19.28z  3861  r19.28zv  3864  r19.37zv  3865  r19.45zv  3866  r19.44zv  3867  r19.27z  3868  r19.27zv  3869  r19.36zv  3870  ralidm  3873  ralsnsg  4003  rexsnsOLD  4005  eldifvsn  4104  ssunsn2  4131  iunconst  4287  iinconst  4288  ordsseleq  5452  funssres  5622  fncnv  5647  fresaun  5754  dff1o5  5823  funimass4  5916  fndmdifeq0  5988  fneqeql2  5991  unpreima  6006  dffo3  6037  fnnfpeq0  6095  funfvima  6140  f1eqcocnv  6199  fliftf  6208  isocnv3  6223  isomin  6228  eloprabga  6383  mpt22eqb  6405  elpwun  6604  dfom2  6694  opabex3d  6771  opabex3  6772  f1oweALT  6777  fnwelem  6911  mptsuppd  6938  dfrecs3  7091  oe0m1  7223  oarec  7263  boxcutc  7565  ordunifi  7821  r1fin  8244  rankr1c  8292  iscard  8409  iscard2  8410  cardval2  8425  dfac3  8552  kmlem8  8587  infinf  8991  xrlenlt  9699  ltxrlt  9704  negcon2  9927  mulne0b  10253  dfinfre  10588  dfinfmrOLD  10589  crne0  10602  elznn  10953  zmax  11261  zq  11270  elfznelfzo  12014  hashneq0  12545  xpcogend  13038  sqrtneglem  13330  rexfiuz  13410  rexanuz2  13412  sumsplit  13829  fsum2dlem  13831  fsumcom2  13835  fprodcom2  14038  odd2np1  14365  divalgb  14385  gcdcllem2  14474  mrcidb2  15524  fncnvimaeqv  16005  lbsacsbs  18379  islpir2  18475  domnmuln0  18522  mplcoe1  18689  mplcoe5  18692  islinds2  19371  islbs4  19390  mamucl  19426  mavmulcl  19572  mdetunilem8  19644  iscld4  20081  iscon2  20429  kgencn  20571  tx1cn  20624  tx2cn  20625  elmptrab  20842  isfbas  20844  fbfinnfr  20856  cnfcf  21057  fmucndlem  21306  prdsxmslem2  21544  blval2  21577  cnbl0  21794  cnblcld  21795  metcld  22275  ismbf  22586  ismbfcn  22587  itg1val2  22642  itg2split  22707  itg2monolem1  22708  aannenlem1  23284  pilem1  23406  sinq34lt0t  23464  ellogrn  23509  logeftb  23533  ercgrg  24562  isusgra0  25074  usgraop  25077  constr3lem2  25374  ch0pss  27098  h1de2ctlem  27208  adjsym  27486  eigposi  27489  dfadj2  27538  elnlfn  27581  xppreima  28248  1stpreima  28287  2ndpreima  28288  qtophaus  28663  prsdm  28720  prsrn  28721  1stmbfm  29082  2ndmbfm  29083  eulerpartlemn  29214  bnj1454  29653  bnj984  29763  nofulllem1  30591  dffun10  30681  hfext  30950  isfne4b  30997  neifg  31027  taupilem3  31720  topdifinfindis  31749  topdifinffinlem  31750  finxpsuclem  31789  poimirlem23  31963  poimirlem26  31966  cnambfre  31989  0totbnd  32105  cvrval2  32840  cvrnbtwn2  32841  cvrnbtwn4  32845  hlateq  32964  islpln5  33100  islvol5  33144  pmap11  33327  4atex  33641  cdleme0ex2N  33790  cdlemefrs29pre00  33962  diaord  34615  dihmeetlem13N  34887  lcfl1  35060  lcfls1N  35103  mapdpglem3  35243  isnacs2  35548  mrefg3  35550  pw2f1ocnv  35892  acsfn1p  36065  relexp0eq  36293  frege124d  36353  sbcoreleleq  36896  dffo3f  37450  climreeq  37693  funressnfv  38629  uhgrvd0nedgb  39545  vdiscusgrb  39567
  Copyright terms: Public domain W3C validator