Theorem syl6rbbr 279

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

Step	Hyp	Ref	Expression
1		syl6rbbr.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		syl6rbbr.2	. . 3 |- ( th <-> ch )
3	2	bicomi 214	. 2 |- ( ch <-> th )
4	1, 3	syl6rbb 277	1 |- ( ph -> ( th <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  baib  944  cad1  1555  necon2abid  2836  reueubd  3164  reu8  3402  sbc6g  3461  r19.28z  4063  r19.37zv  4067  r19.45zv  4068  r19.44zv  4069  r19.27z  4070  r19.36zv  4072  ralidm  4075  ralsnsg  4216  eldifvsn  4326  ssunsn2  4359  iunconst  4529  iinconst  4530  ordsseleq  5752  ordequn  5828  funssres  5930  fncnv  5962  fresaun  6075  dff1o5  6146  funimass4  6247  fndmdifeq0  6323  fneqeql2  6326  unpreima  6341  dffo3  6374  fnnfpeq0  6444  funfvima  6492  f1eqcocnv  6556  fliftf  6565  isocnv3  6582  isomin  6587  eloprabga  6747  mpt22eqb  6769  elpwun  6977  dfom2  7067  opabex3d  7145  opabex3  7146  f1oweALT  7152  fnwelem  7292  mptsuppd  7318  dfrecs3  7469  oe0m1  7601  oarec  7642  boxcutc  7951  ordunifi  8210  r1fin  8636  rankr1c  8684  iscard  8801  iscard2  8802  cardval2  8817  dfac3  8944  kmlem8  8979  infinf  9388  xrlenlt  10103  ltxrlt  10108  negcon2  10334  mulne0b  10668  dfinfre  11004  crne0  11013  elznn  11393  zmax  11785  zq  11794  elfznelfzo  12573  modmuladdnn0  12714  hashneq0  13155  xpcogend  13713  sqrtneglem  14007  rexfiuz  14087  rexanuz2  14089  sumsplit  14499  fsum2dlem  14501  fsumcom2OLD  14506  fprodcom2OLD  14715  odd2np1  15065  divalgb  15127  gcdcllem2  15222  mrcidb2  16278  fncnvimaeqv  16760  lbsacsbs  19156  islpir2  19251  domnmuln0  19298  mplcoe1  19465  mplcoe5  19468  islinds2  20152  islbs4  20171  mamucl  20207  mavmulcl  20353  mdetunilem8  20425  iscld4  20869  isconn2  21217  kgencn  21359  tx1cn  21412  tx2cn  21413  elmptrab  21630  isfbas  21633  fbfinnfr  21645  cnfcf  21846  fmucndlem  22095  prdsxmslem2  22334  blval2  22367  cnbl0  22577  cnblcld  22578  metcld  23104  ismbf  23397  ismbfcn  23398  itg1val2  23451  itg2split  23516  itg2monolem1  23517  aannenlem1  24083  pilem1  24205  sinq34lt0t  24261  ellogrn  24306  logeftb  24330  gausslemma2dlem1a  25090  ercgrg  25412  usgredgffibi  26216  vtxd0nedgb  26384  vdiscusgrb  26426  upgrspthswlk  26634  s3wwlks2on  26849  frgrncvvdeqlem2  27164  ch0pss  28304  h1de2ctlem  28414  adjsym  28692  eigposi  28695  dfadj2  28744  elnlfn  28787  xppreima  29449  1stpreima  29484  2ndpreima  29485  qtophaus  29903  prsdm  29960  prsrn  29961  1stmbfm  30322  2ndmbfm  30323  eulerpartlemn  30443  reprdifc  30705  circlemeth  30718  bnj1454  30912  bnj984  31022  elintfv  31662  dffun10  32021  hfext  32290  isfne4b  32336  neifg  32366  taupilem3  33165  topdifinfindis  33194  topdifinffinlem  33195  finxpsuclem  33234  poimirlem23  33432  poimirlem26  33435  cnambfre  33458  0totbnd  33572  opelvvdif  34023  opelresALTV  34031  inecmo  34120  19.9alt  34252  cvrval2  34561  cvrnbtwn2  34562  cvrnbtwn4  34566  hlateq  34685  islpln5  34821  islvol5  34865  pmap11  35048  4atex  35362  cdleme0ex2N  35511  cdlemefrs29pre00  35683  diaord  36336  dihmeetlem13N  36608  lcfl1  36781  lcfls1N  36824  mapdpglem3  36964  isnacs2  37269  mrefg3  37271  pw2f1ocnv  37604  acsfn1p  37769  relexp0eq  37993  frege124d  38053  uneqsn  38321  k0004lem1  38445  sbcoreleleq  38745  dffo3f  39364  climreeq  39845  funressnfv  41208  fmtnorec2lem  41454