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  909  pm5.63dc  948  pm4.83dc  953  pm5.71dc  963  19.33b2  1643  19.9t  1656  sb4b  1848  a16gb  1879  euor2  2103  eupickbi  2127  ceqsalg  2791  eqvincg  2888  ddifstab  3296  csbprc  3497  undif4  3514  eqifdc  3597  ifnebibdc  3605  sssnm  3785  sneqbg  3794  opthpr  3803  elpwuni  4007  ss1o0el1  4231  exmid01  4232  exmidundif  4240  eusv2i  4491  reusv3  4496  iunpw  4516  suc11g  4594  ssxpbm  5106  ssxp1  5107  ssxp2  5108  xp11m  5109  2elresin  5372  mpteqb  5655  f1fveq  5822  f1elima  5823  f1imass  5824  fliftf  5849  nnsucuniel  6562  iserd  6627  ecopovtrn  6700  ecopover  6701  ecopovtrng  6703  ecopoverg  6704  map0g  6756  fopwdom  6906  f1finf1o  7022  mkvprop  7233  addcanpig  7418  mulcanpig  7419  srpospr  7867  readdcan  8183  cnegexlem1  8218  addcan  8223  addcan2  8224  neg11  8294  negreb  8308  add20  8518  cru  8646  mulcanapd  8705  uz11  9641  eqreznegel  9705  lbzbi  9707  xneg11  9926  xnn0xadd0  9959  xsubge0  9973  elioc2  10028  elico2  10029  elicc2  10030  fzopth  10153  2ffzeq  10233  flqidz  10393  addmodlteq  10507  frec2uzrand  10514  nninfinf  10552  expcan  10825  nn0opthd  10831  fz1eqb  10899  wrdnval  10982  eqwrd  10992  cj11  11087  sqrt0  11186  recan  11291  0dvds  11993  dvds1  12035  alzdvds  12036  nn0enne  12084  nn0oddm1d2  12091  nnoddm1d2  12092  divalgmod  12109  gcdeq0  12169  algcvgblem  12242  prmexpb  12344  4sqexercise2  12593  4sqlemsdc  12594  4sqlem11  12595  ennnfonelemim  12666  grprcan  13239  grplcan  13264  grpinv11  13271  isnzr2  13816  znidomb  14290  tgdom  14392  en1top  14397  hmeocnvb  14638  metrest  14826  perfect  15321  lgsne0  15363  2lgs  15429  2lgsoddprmlem3  15436  bj-nnbist  15474  bj-nnbidc  15487  bj-peano4  15685  bj-nn0sucALT  15708