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  848  pm5.63dc  888  pm4.83dc  893  pm5.71dc  903  19.33b2  1561  19.9t  1574  sb4b  1756  a16gb  1787  euor2  2000  eupickbi  2024  ceqsalg  2628  eqvincg  2720  ddifstab  3105  csbprc  3296  undif4  3313  sssnm  3554  sneqbg  3563  opthpr  3572  elpwuni  3770  eusv2i  4213  reusv3  4218  iunpw  4237  suc11g  4308  xpid11m  4585  ssxpbm  4786  ssxp1  4787  ssxp2  4788  xp11m  4789  2elresin  5041  mpteqb  5293  f1fveq  5443  f1elima  5444  f1imass  5445  fliftf  5470  nnsucuniel  6139  iserd  6198  ecopovtrn  6269  ecopover  6270  ecopovtrng  6272  ecopoverg  6273  fopwdom  6380  addcanpig  6586  mulcanpig  6587  srpospr  7021  readdcan  7315  cnegexlem1  7350  addcan  7355  addcan2  7356  neg11  7426  negreb  7440  add20  7645  cru  7769  mulcanapd  7818  uz11  8722  eqreznegel  8780  lbzbi  8782  xneg11  8977  elioc2  9035  elico2  9036  elicc2  9037  fzopth  9155  2ffzeq  9228  flqidz  9368  addmodlteq  9480  frec2uzrand  9487  expcan  9741  nn0opthd  9746  fz1eqb  9815  cj11  9930  sqrt0  10028  recan  10133  0dvds  10360  dvds1  10398  alzdvds  10399  nn0enne  10446  nn0oddm1d2  10453  nnoddm1d2  10454  divalgmod  10471  gcdeq0  10512  algcvgblem  10575  prmexpb  10674  bj-peano4  10908  bj-nn0sucALT  10931