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

Theorem syl6rbbr 256
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 194 . 2  |-  ( ch  <->  th )
41, 3syl6rbb 254 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  baib  872  reu8  3090  sbc6g  3146  r19.28z  3680  r19.28zv  3683  r19.37zv  3684  r19.45zv  3685  r19.27z  3686  r19.27zv  3687  r19.36zv  3688  ralidm  3691  ralsns  3804  rexsns  3805  ssunsn2  3918  iunconst  4061  iinconst  4062  ordsseleq  4570  reusv7OLD  4694  elpwun  4715  dfom2  4806  funssres  5452  fncnv  5474  fresaun  5573  dff1o5  5642  funimass4  5736  fndmdifeq0  5795  fneqeql2  5798  unpreima  5815  dffo3  5843  funfvima  5932  opabex3d  5948  opabex3  5949  f1eqcocnv  5987  fliftf  5996  isocnv3  6011  isomin  6016  f1oweALT  6033  eloprabga  6119  mpt22eqb  6138  fnwelem  6420  oe0m1  6724  oarec  6764  boxcutc  7064  ordunifi  7316  r1fin  7655  rankr1c  7703  iscard  7818  iscard2  7819  cardval2  7834  dfac3  7958  kmlem8  7993  infinf  8397  xrlenlt  9099  ltxrlt  9102  negcon2  9310  mulne0b  9619  dfinfmr  9941  crne0  9949  elznn  10253  zmax  10527  zq  10536  elfznelfzo  11147  sqrneglem  12027  rexanuz2  12108  sumsplit  12507  fsum2dlem  12509  fsumcom2  12513  odd2np1  12863  divalgb  12879  gcdcllem2  12967  mrcidb2  13798  lbsacsbs  16183  islpir2  16277  domnmuln0  16313  mplcoe1  16483  mplcoe2  16485  iscld4  17084  iscon2  17430  kgencn  17541  tx1cn  17594  tx2cn  17595  elmptrab  17812  isfbas  17814  fbfinnfr  17826  cnfcf  18027  fmucndlem  18274  prdsxmslem2  18512  blval2  18558  cnbl0  18761  cnblcld  18762  metcld  19211  ismbf  19475  ismbfcn  19476  itg1val2  19529  itg2split  19594  itg2monolem1  19595  aannenlem1  20198  pilem1  20320  sinq34lt0t  20370  ellogrn  20410  logeftb  20431  isusgra0  21329  constr3lem2  21586  ch0pss  22900  h1de2ctlem  23010  adjsym  23289  eigposi  23292  dfadj2  23341  elnlfn  23384  xppreima  24012  1stpreima  24048  2ndpreima  24049  1stmbfm  24563  2ndmbfm  24564  fprodcom2  25261  nofulllem1  25570  hfext  26028  cnambfre  26154  isfne4b  26240  neifg  26290  0totbnd  26372  fnnfpeq0  26629  isnacs2  26650  mrefg3  26652  pw2f1ocnv  26998  islinds2  27151  islbs4  27170  mamucl  27324  acsfn1p  27375  climreeq  27606  funressnfv  27859  bnj1454  28919  bnj984  29029  cvrval2  29757  cvrnbtwn2  29758  cvrnbtwn4  29762  hlateq  29881  islpln5  30017  islvol5  30061  pmap11  30244  4atex  30558  cdleme0ex2N  30706  cdlemefrs29pre00  30877  diaord  31530  dihmeetlem13N  31802  lcfl1  31975  lcfls1N  32018  mapdpglem3  32158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator