Theorem impbid1 141

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  iba  296  ibar  297  pm4.81dc  858  pm5.63dc  898  pm4.83dc  903  pm5.71dc  913  19.33b2  1576  19.9t  1589  sb4b  1773  a16gb  1804  euor2  2018  eupickbi  2042  ceqsalg  2669  eqvincg  2763  ddifstab  3155  csbprc  3355  undif4  3372  eqifdc  3453  sssnm  3628  sneqbg  3637  opthpr  3646  elpwuni  3848  exmid01  4061  exmidundif  4067  eusv2i  4314  reusv3  4319  iunpw  4339  suc11g  4410  ssxpbm  4910  ssxp1  4911  ssxp2  4912  xp11m  4913  2elresin  5170  mpteqb  5443  f1fveq  5605  f1elima  5606  f1imass  5607  fliftf  5632  nnsucuniel  6321  iserd  6385  ecopovtrn  6456  ecopover  6457  ecopovtrng  6459  ecopoverg  6460  map0g  6512  fopwdom  6659  f1finf1o  6763  mkvprop  6943  addcanpig  7043  mulcanpig  7044  srpospr  7478  readdcan  7773  cnegexlem1  7808  addcan  7813  addcan2  7814  neg11  7884  negreb  7898  add20  8103  cru  8230  mulcanapd  8283  uz11  9198  eqreznegel  9256  lbzbi  9258  xneg11  9458  xnn0xadd0  9491  xsubge0  9505  elioc2  9560  elico2  9561  elicc2  9562  fzopth  9682  2ffzeq  9759  flqidz  9900  addmodlteq  10012  frec2uzrand  10019  expcan  10304  nn0opthd  10309  fz1eqb  10378  cj11  10518  sqrt0  10616  recan  10721  0dvds  11308  dvds1  11346  alzdvds  11347  nn0enne  11394  nn0oddm1d2  11401  nnoddm1d2  11402  divalgmod  11419  gcdeq0  11460  algcvgblem  11523  prmexpb  11622  ennnfonelemim  11729  tgdom  12023  en1top  12028  metrest  12434  bj-peano4  12738  bj-nn0sucALT  12761