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  936  pm4.83dc  941  pm5.71dc  951  19.33b2  1617  19.9t  1630  sb4b  1822  a16gb  1853  euor2  2072  eupickbi  2096  ceqsalg  2754  eqvincg  2850  ddifstab  3254  csbprc  3454  undif4  3471  eqifdc  3554  sssnm  3734  sneqbg  3743  opthpr  3752  elpwuni  3955  ss1o0el1  4176  exmid01  4177  exmidundif  4185  eusv2i  4433  reusv3  4438  iunpw  4458  suc11g  4534  ssxpbm  5039  ssxp1  5040  ssxp2  5041  xp11m  5042  2elresin  5299  mpteqb  5576  f1fveq  5740  f1elima  5741  f1imass  5742  fliftf  5767  nnsucuniel  6463  iserd  6527  ecopovtrn  6598  ecopover  6599  ecopovtrng  6601  ecopoverg  6602  map0g  6654  fopwdom  6802  f1finf1o  6912  mkvprop  7122  addcanpig  7275  mulcanpig  7276  srpospr  7724  readdcan  8038  cnegexlem1  8073  addcan  8078  addcan2  8079  neg11  8149  negreb  8163  add20  8372  cru  8500  mulcanapd  8558  uz11  9488  eqreznegel  9552  lbzbi  9554  xneg11  9770  xnn0xadd0  9803  xsubge0  9817  elioc2  9872  elico2  9873  elicc2  9874  fzopth  9996  2ffzeq  10076  flqidz  10221  addmodlteq  10333  frec2uzrand  10340  expcan  10629  nn0opthd  10635  fz1eqb  10704  cj11  10847  sqrt0  10946  recan  11051  0dvds  11751  dvds1  11791  alzdvds  11792  nn0enne  11839  nn0oddm1d2  11846  nnoddm1d2  11847  divalgmod  11864  gcdeq0  11910  algcvgblem  11981  prmexpb  12083  ennnfonelemim  12357  tgdom  12712  en1top  12717  hmeocnvb  12958  metrest  13146  lgsne0  13579  bj-nnbist  13625  bj-nnbidc  13638  bj-peano4  13837  bj-nn0sucALT  13860