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  8020  negcon2  8208  dfinfre  8911  sup3exmid  8912  elznn  9267  zq  9624  rpnegap  9684  modqmuladdnn0  10365  shftdm  10826  rexfiuz  10993  rexanuz2  10995  sumsplitdc  11435  fsum2dlemstep  11437  odd2np1  11872  divalgb  11924  infssuzex  11944  isprm4  12113  ctiunctlemudc  12432  grp1  12930  nmznsg  13026  iscrng2  13151  tx1cn  13662  tx2cn  13663  cnbl0  13927  cnblcld  13928  reopnap  13931  pilem1  14093  sinq34lt0t  14145