Theorem impbid1 142

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  impbid2  143  iba  300  ibar  301  pm4.81dc  908  pm5.63dc  946  pm4.83dc  951  pm5.71dc  961  19.33b2  1629  19.9t  1642  sb4b  1834  a16gb  1865  euor2  2084  eupickbi  2108  ceqsalg  2765  eqvincg  2861  ddifstab  3267  csbprc  3468  undif4  3485  eqifdc  3569  sssnm  3753  sneqbg  3762  opthpr  3771  elpwuni  3974  ss1o0el1  4195  exmid01  4196  exmidundif  4204  eusv2i  4453  reusv3  4458  iunpw  4478  suc11g  4554  ssxpbm  5061  ssxp1  5062  ssxp2  5063  xp11m  5064  2elresin  5324  mpteqb  5603  f1fveq  5768  f1elima  5769  f1imass  5770  fliftf  5795  nnsucuniel  6491  iserd  6556  ecopovtrn  6627  ecopover  6628  ecopovtrng  6630  ecopoverg  6631  map0g  6683  fopwdom  6831  f1finf1o  6941  mkvprop  7151  addcanpig  7328  mulcanpig  7329  srpospr  7777  readdcan  8091  cnegexlem1  8126  addcan  8131  addcan2  8132  neg11  8202  negreb  8216  add20  8425  cru  8553  mulcanapd  8612  uz11  9544  eqreznegel  9608  lbzbi  9610  xneg11  9828  xnn0xadd0  9861  xsubge0  9875  elioc2  9930  elico2  9931  elicc2  9932  fzopth  10054  2ffzeq  10134  flqidz  10279  addmodlteq  10391  frec2uzrand  10398  expcan  10687  nn0opthd  10693  fz1eqb  10761  cj11  10905  sqrt0  11004  recan  11109  0dvds  11809  dvds1  11849  alzdvds  11850  nn0enne  11897  nn0oddm1d2  11904  nnoddm1d2  11905  divalgmod  11922  gcdeq0  11968  algcvgblem  12039  prmexpb  12141  ennnfonelemim  12415  grprcan  12838  grplcan  12860  grpinv11  12867  tgdom  13354  en1top  13359  hmeocnvb  13600  metrest  13788  lgsne0  14221  bj-nnbist  14267  bj-nnbidc  14280  bj-peano4  14478  bj-nn0sucALT  14501