Theorem impbid1 140

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 127	1 |- ( ph -> ( ps <-> ch ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  impbid2  141  iba  294  ibar  295  pm4.81dc  850  pm5.63dc  890  pm4.83dc  895  pm5.71dc  905  19.33b2  1563  19.9t  1576  sb4b  1759  a16gb  1790  euor2  2003  eupickbi  2027  ceqsalg  2641  eqvincg  2732  ddifstab  3121  csbprc  3316  undif4  3333  eqifdc  3411  sssnm  3583  sneqbg  3592  opthpr  3601  elpwuni  3799  exmid01  4008  exmidundif  4011  eusv2i  4253  reusv3  4258  iunpw  4277  suc11g  4348  xpid11m  4628  ssxpbm  4834  ssxp1  4835  ssxp2  4836  xp11m  4837  2elresin  5092  mpteqb  5358  f1fveq  5514  f1elima  5515  f1imass  5516  fliftf  5541  nnsucuniel  6212  iserd  6272  ecopovtrn  6343  ecopover  6344  ecopovtrng  6346  ecopoverg  6347  map0g  6399  fopwdom  6506  f1finf1o  6608  addcanpig  6840  mulcanpig  6841  srpospr  7275  readdcan  7569  cnegexlem1  7604  addcan  7609  addcan2  7610  neg11  7680  negreb  7694  add20  7899  cru  8023  mulcanapd  8072  uz11  8976  eqreznegel  9034  lbzbi  9036  xneg11  9231  elioc2  9289  elico2  9290  elicc2  9291  fzopth  9409  2ffzeq  9483  flqidz  9624  addmodlteq  9736  frec2uzrand  9743  expcan  10025  nn0opthd  10030  fz1eqb  10099  cj11  10238  sqrt0  10336  recan  10441  0dvds  10722  dvds1  10760  alzdvds  10761  nn0enne  10808  nn0oddm1d2  10815  nnoddm1d2  10816  divalgmod  10833  gcdeq0  10874  algcvgblem  10937  prmexpb  11036  bj-peano4  11319  bj-nn0sucALT  11342