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  904  cad1  1483  necon2abid  2657  reu8  3245  sbc6g  3303  r19.28z  3865  r19.28zv  3868  r19.37zv  3869  r19.45zv  3870  r19.44zv  3871  r19.27z  3872  r19.27zv  3873  r19.36zv  3874  ralidm  3877  ralsnsg  4004  rexsnsOLD  4006  eldifvsn  4104  ssunsn2  4131  iunconst  4280  iinconst  4281  ordsseleq  5439  funssres  5609  fncnv  5633  fresaun  5739  dff1o5  5808  funimass4  5900  fndmdifeq0  5971  fneqeql2  5974  unpreima  5991  dffo3  6024  fnnfpeq0  6082  funfvima  6128  f1eqcocnv  6187  fliftf  6196  isocnv3  6211  isomin  6216  eloprabga  6370  mpt22eqb  6392  elpwun  6595  dfom2  6685  opabex3d  6762  opabex3  6763  f1oweALT  6768  fnwelem  6899  mptsuppd  6926  dfrecs3  7076  oe0m1  7208  oarec  7248  boxcutc  7550  ordunifi  7804  r1fin  8223  rankr1c  8271  iscard  8388  iscard2  8389  cardval2  8404  dfac3  8534  kmlem8  8569  infinf  8973  xrlenlt  9682  ltxrlt  9686  negcon2  9908  mulne0b  10231  dfinfmr  10560  crne0  10569  elznn  10921  zmax  11224  zq  11233  elfznelfzo  11952  hashneq0  12482  xpcogend  12957  sqrtneglem  13249  rexfiuz  13329  rexanuz2  13331  sumsplit  13734  fsum2dlem  13736  fsumcom2  13740  fprodcom2  13940  odd2np1  14255  divalgb  14271  gcdcllem2  14359  mrcidb2  15232  fncnvimaeqv  15713  lbsacsbs  18122  islpir2  18219  domnmuln0  18267  mplcoe1  18447  mplcoe5  18451  mplcoe2OLD  18453  islinds2  19140  islbs4  19159  mamucl  19195  mavmulcl  19341  mdetunilem8  19413  iscld4  19859  iscon2  20207  kgencn  20349  tx1cn  20402  tx2cn  20403  elmptrab  20620  isfbas  20622  fbfinnfr  20634  cnfcf  20835  fmucndlem  21086  prdsxmslem2  21324  blval2  21370  cnbl0  21573  cnblcld  21574  metcld  22036  ismbf  22329  ismbfcn  22330  itg1val2  22383  itg2split  22448  itg2monolem1  22449  aannenlem1  23016  pilem1  23138  sinq34lt0t  23194  ellogrn  23239  logeftb  23263  ercgrg  24289  isusgra0  24764  usgraop  24767  constr3lem2  25063  ch0pss  26777  h1de2ctlem  26887  adjsym  27165  eigposi  27168  dfadj2  27217  elnlfn  27260  xppreima  27930  1stpreima  27969  2ndpreima  27970  qtophaus  28292  prsdm  28349  prsrn  28350  1stmbfm  28708  2ndmbfm  28709  eulerpartlemn  28826  bnj1454  29227  bnj984  29337  nofulllem1  30162  dffun10  30252  hfext  30521  isfne4b  30569  neifg  30599  taupilem3  31245  topdifinfindis  31263  topdifinffinlem  31264  cnambfre  31435  0totbnd  31551  cvrval2  32292  cvrnbtwn2  32293  cvrnbtwn4  32297  hlateq  32416  islpln5  32552  islvol5  32596  pmap11  32779  4atex  33093  cdleme0ex2N  33242  cdlemefrs29pre00  33414  diaord  34067  dihmeetlem13N  34339  lcfl1  34512  lcfls1N  34555  mapdpglem3  34695  isnacs2  35000  mrefg3  35002  pw2f1ocnv  35341  acsfn1p  35512  relexp0eq  35680  frege124d  35740  sbcoreleleq  36326  climreeq  36987  funressnfv  37581
  Copyright terms: Public domain W3C validator