Theorem syl6rbbr 198

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 131	. 2 |- ( ch <-> th )
4	1, 3	syl6rbb 196	1 |- ( ph -> ( th <-> ps ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imimorbdc  862  baib  885  pm5.6dc  892  xornbidc  1350  mo2dc  2028  reu8  2847  sbc6g  2900  dfss4st  3273  r19.28m  3416  r19.45mv  3420  r19.44mv  3421  r19.27m  3422  ralsnsg  3525  ralsns  3526  iunconstm  3785  iinconstm  3786  exmidsssnc  4084  unisucg  4294  relsng  4600  funssres  5121  fncnv  5145  dff1o5  5330  funimass4  5424  fneqeql2  5481  fnniniseg2  5495  rexsupp  5496  unpreima  5497  dffo3  5519  funfvima  5601  dff13  5621  f1eqcocnv  5644  fliftf  5652  isocnv2  5665  eloprabga  5810  mpo2eqb  5832  opabex3d  5971  opabex3  5972  elxp6  6019  elxp7  6020  sbthlemi5  6799  sbthlemi6  6800  genpdflem  7257  ltnqpr  7343  ltexprlemloc  7357  xrlenlt  7747  negcon2  7932  dfinfre  8618  sup3exmid  8619  elznn  8968  zq  9314  rpnegap  9369  modqmuladdnn0  10028  shftdm  10481  rexfiuz  10647  rexanuz2  10649  sumsplitdc  11087  fsum2dlemstep  11089  odd2np1  11412  divalgb  11464  infssuzex  11484  isprm4  11640  ctiunctlemudc  11787  tx1cn  12274  tx2cn  12275  cnbl0  12517  cnblcld  12518