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-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  iba  298  ibar  299  pm4.81dc  898  pm5.63dc  935  pm4.83dc  940  pm5.71dc  950  19.33b2  1616  19.9t  1629  sb4b  1821  a16gb  1852  euor2  2071  eupickbi  2095  ceqsalg  2749  eqvincg  2845  ddifstab  3249  csbprc  3449  undif4  3466  eqifdc  3549  sssnm  3728  sneqbg  3737  opthpr  3746  elpwuni  3949  ss1o0el1  4170  exmid01  4171  exmidundif  4179  eusv2i  4427  reusv3  4432  iunpw  4452  suc11g  4528  ssxpbm  5033  ssxp1  5034  ssxp2  5035  xp11m  5036  2elresin  5293  mpteqb  5570  f1fveq  5734  f1elima  5735  f1imass  5736  fliftf  5761  nnsucuniel  6454  iserd  6518  ecopovtrn  6589  ecopover  6590  ecopovtrng  6592  ecopoverg  6593  map0g  6645  fopwdom  6793  f1finf1o  6903  mkvprop  7113  addcanpig  7266  mulcanpig  7267  srpospr  7715  readdcan  8029  cnegexlem1  8064  addcan  8069  addcan2  8070  neg11  8140  negreb  8154  add20  8363  cru  8491  mulcanapd  8549  uz11  9479  eqreznegel  9543  lbzbi  9545  xneg11  9761  xnn0xadd0  9794  xsubge0  9808  elioc2  9863  elico2  9864  elicc2  9865  fzopth  9986  2ffzeq  10066  flqidz  10211  addmodlteq  10323  frec2uzrand  10330  expcan  10618  nn0opthd  10624  fz1eqb  10693  cj11  10833  sqrt0  10932  recan  11037  0dvds  11737  dvds1  11776  alzdvds  11777  nn0enne  11824  nn0oddm1d2  11831  nnoddm1d2  11832  divalgmod  11849  gcdeq0  11895  algcvgblem  11960  prmexpb  12060  ennnfonelemim  12294  tgdom  12613  en1top  12618  hmeocnvb  12859  metrest  13047  bj-nnbist  13460  bj-nnbidc  13471  bj-peano4  13672  bj-nn0sucALT  13695