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  2721  reu8  3299  sbc6g  3357  r19.28z  3920  r19.28zv  3923  r19.37zv  3924  r19.45zv  3925  r19.27z  3926  r19.27zv  3927  r19.36zv  3928  ralidm  3931  ralsnsg  4059  rexsnsOLD  4061  eldifvsn  4159  ssunsn2  4186  iunconst  4334  iinconst  4335  reusv7OLD  4659  ordsseleq  4907  funssres  5628  fncnv  5652  fresaun  5756  dff1o5  5825  funimass4  5918  fndmdifeq0  5987  fneqeql2  5990  unpreima  6007  dffo3  6036  fnnfpeq0  6092  funfvima  6135  f1eqcocnv  6192  fliftf  6201  isocnv3  6216  isomin  6221  eloprabga  6373  mpt22eqb  6395  elpwun  6597  dfom2  6686  opabex3d  6762  opabex3  6763  f1oweALT  6768  fnwelem  6898  mptsuppd  6923  oe0m1  7171  oarec  7211  boxcutc  7512  ordunifi  7770  r1fin  8191  rankr1c  8239  iscard  8356  iscard2  8357  cardval2  8372  dfac3  8502  kmlem8  8537  infinf  8941  xrlenlt  9652  ltxrlt  9655  negcon2  9872  mulne0b  10190  dfinfmr  10520  crne0  10529  elznn  10880  zmax  11179  zq  11188  elfznelfzo  11883  hashneq0  12402  sqrtneglem  13063  rexfiuz  13143  rexanuz2  13145  sumsplit  13546  fsum2dlem  13548  fsumcom2  13552  odd2np1  13905  divalgb  13921  gcdcllem2  14009  mrcidb2  14873  lbsacsbs  17602  islpir2  17698  domnmuln0  17746  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  islinds2  18643  islbs4  18662  mamucl  18698  mavmulcl  18844  mdetunilem8  18916  iscld4  19360  iscon2  19709  kgencn  19820  tx1cn  19873  tx2cn  19874  elmptrab  20091  isfbas  20093  fbfinnfr  20105  cnfcf  20306  fmucndlem  20557  prdsxmslem2  20795  blval2  20841  cnbl0  21044  cnblcld  21045  metcld  21507  ismbf  21800  ismbfcn  21801  itg1val2  21854  itg2split  21919  itg2monolem1  21920  aannenlem1  22486  pilem1  22608  sinq34lt0t  22663  ellogrn  22703  logeftb  22724  ercgrg  23664  isusgra0  24051  usgraop  24054  constr3lem2  24350  ch0pss  26067  h1de2ctlem  26177  adjsym  26456  eigposi  26459  dfadj2  26508  elnlfn  26551  xppreima  27187  1stpreima  27224  2ndpreima  27225  prsdm  27560  prsrn  27561  qtophaus  27665  1stmbfm  27899  2ndmbfm  27900  eulerpartlemn  27988  fprodcom2  28719  nofulllem1  29067  dffun10  29169  hfext  29445  cnambfre  29668  isfne4b  29770  neifg  29820  0totbnd  29900  isnacs2  30270  mrefg3  30272  pw2f1ocnv  30611  acsfn1p  30781  climreeq  31183  funressnfv  31708  sbcoreleleq  32403  bnj1454  32997  bnj984  33107  cvrval2  34089  cvrnbtwn2  34090  cvrnbtwn4  34094  hlateq  34213  islpln5  34349  islvol5  34393  pmap11  34576  4atex  34890  cdleme0ex2N  35038  cdlemefrs29pre00  35209  diaord  35862  dihmeetlem13N  36134  lcfl1  36307  lcfls1N  36350  mapdpglem3  36490  taupilem3  36782  xpcogend  36801
  Copyright terms: Public domain W3C validator