Theorem bitr4id 199

Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)

Hypotheses

Ref	Expression
bitr4id.2	|- ( ps <-> ch )
bitr4id.1	|- ( ph -> ( th <-> ch ) )

Assertion

Ref	Expression
bitr4id	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitr4id

Step	Hyp	Ref	Expression
1		bitr4id.1	. 2 |- ( ph -> ( th <-> ch ) )
2		bitr4id.2	. . 3 |- ( ps <-> ch )
3	2	bicomi 132	. 2 |- ( ch <-> ps )
4	1, 3	bitr2di 197	1 |- ( ph -> ( ps <-> th ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imimorbdc  896  baib  919  pm5.6dc  926  xornbidc  1391  mo2dc  2081  reu8  2933  sbc6g  2987  dfss4st  3368  r19.28m  3512  r19.45mv  3516  r19.44mv  3517  r19.27m  3518  ralsnsg  3629  ralsns  3630  iunconstm  3894  iinconstm  3895  exmidsssnc  4203  unisucg  4414  relsng  4729  funssres  5258  fncnv  5282  dff1o5  5470  funimass4  5566  fneqeql2  5625  fnniniseg2  5639  rexsupp  5640  unpreima  5641  dffo3  5663  funfvima  5748  dff13  5768  f1eqcocnv  5791  fliftf  5799  isocnv2  5812  eloprabga  5961  mpo2eqb  5983  opabex3d  6121  opabex3  6122  elxp6  6169  elxp7  6170  sbthlemi5  6959  sbthlemi6  6960  nninfwlporlemd  7169  genpdflem  7505  ltnqpr  7591  ltexprlemloc  7605  xrlenlt  8021  negcon2  8209  dfinfre  8912  sup3exmid  8913  elznn  9268  zq  9625  rpnegap  9685  modqmuladdnn0  10367  shftdm  10830  rexfiuz  10997  rexanuz2  10999  sumsplitdc  11439  fsum2dlemstep  11441  odd2np1  11877  divalgb  11929  infssuzex  11949  isprm4  12118  ctiunctlemudc  12437  grp1  12975  nmznsg  13071  iscrng2  13196  tx1cn  13739  tx2cn  13740  cnbl0  14004  cnblcld  14005  reopnap  14008  pilem1  14170  sinq34lt0t  14222