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  910  pm5.63dc  949  pm4.83dc  954  pm5.71dc  964  19.33b2  1652  19.9t  1665  sb4b  1857  a16gb  1888  euor2  2112  eupickbi  2136  ceqsalg  2800  eqvincg  2897  ddifstab  3305  csbprc  3506  undif4  3523  eqifdc  3607  ifnebibdc  3615  sssnm  3795  sneqbg  3804  opthpr  3813  elpwuni  4017  ss1o0el1  4242  exmid01  4243  exmidundif  4251  eusv2i  4503  reusv3  4508  iunpw  4528  suc11g  4606  ssxpbm  5119  ssxp1  5120  ssxp2  5121  xp11m  5122  2elresin  5388  mpteqb  5672  f1fveq  5843  f1elima  5844  f1imass  5845  fliftf  5870  nnsucuniel  6583  iserd  6648  ecopovtrn  6721  ecopover  6722  ecopovtrng  6724  ecopoverg  6725  map0g  6777  fopwdom  6935  f1finf1o  7051  mkvprop  7262  addcanpig  7449  mulcanpig  7450  srpospr  7898  readdcan  8214  cnegexlem1  8249  addcan  8254  addcan2  8255  neg11  8325  negreb  8339  add20  8549  cru  8677  mulcanapd  8736  uz11  9673  eqreznegel  9737  lbzbi  9739  xneg11  9958  xnn0xadd0  9991  xsubge0  10005  elioc2  10060  elico2  10061  elicc2  10062  fzopth  10185  2ffzeq  10265  flqidz  10431  addmodlteq  10545  frec2uzrand  10552  nninfinf  10590  expcan  10863  nn0opthd  10869  fz1eqb  10937  wrdnval  11026  eqwrd  11036  wrdl1s1  11087  cj11  11249  sqrt0  11348  recan  11453  0dvds  12155  dvds1  12197  alzdvds  12198  nn0enne  12246  nn0oddm1d2  12253  nnoddm1d2  12254  divalgmod  12271  gcdeq0  12331  algcvgblem  12404  prmexpb  12506  4sqexercise2  12755  4sqlemsdc  12756  4sqlem11  12757  ennnfonelemim  12828  grprcan  13402  grplcan  13427  grpinv11  13434  isnzr2  13979  znidomb  14453  tgdom  14577  en1top  14582  hmeocnvb  14823  metrest  15011  perfect  15506  lgsne0  15548  2lgs  15614  2lgsoddprmlem3  15621  bj-nnbist  15717  bj-nnbidc  15730  bj-peano4  15928  bj-nn0sucALT  15951