Theorem impbid1 130

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1	|- ( ph -> ( ps -> ch ) )
impbid1.2	|- ( ch -> ps )

Assertion

Ref	Expression
impbid1	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 |- ( ph -> ( ps -> ch ) )
2		impbid1.2	. . 3 |- ( ch -> ps )
3	2	a1i 9	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	impbid 120	1 |- ( ph -> ( ps <-> ch ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  impbid2  131  iba  284  ibar  285  pm4.81dc  814  pm5.63dc  853  pm4.83dc  858  pm5.71dc  868  19.33b2  1520  19.9t  1533  sb4b  1715  a16gb  1745  euor2  1958  eupickbi  1982  ceqsalg  2582  eqvincg  2668  csbprc  3262  undif4  3284  sssnm  3525  sneqbg  3534  opthpr  3543  elpwuni  3741  eusv2i  4187  reusv3  4192  iunpw  4211  suc11g  4281  xpid11m  4557  ssxpbm  4756  ssxp1  4757  ssxp2  4758  xp11m  4759  2elresin  5010  mpteqb  5261  f1fveq  5411  f1elima  5412  f1imass  5413  fliftf  5439  iserd  6132  ecopovtrn  6203  ecopover  6204  ecopovtrng  6206  ecopoverg  6207  fopwdom  6310  addcanpig  6432  mulcanpig  6433  srpospr  6867  readdcan  7153  cnegexlem1  7186  addcan  7191  addcan2  7192  neg11  7262  negreb  7276  add20  7469  cru  7593  mulcanapd  7642  uz11  8495  eqreznegel  8549  lbzbi  8551  xneg11  8747  elioc2  8805  elico2  8806  elicc2  8807  fzopth  8924  2ffzeq  8998  flqidz  9128  frec2uzrand  9191  cj11  9505  sqrt0  9602  recan  9705  algcvgblem  9888  bj-peano4  10080  bj-nn0sucALT  10103