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  913  pm5.63dc  952  pm4.83dc  957  pm5.71dc  967  19.33b2  1675  19.9t  1688  sb4b  1880  a16gb  1911  euor2  2136  eupickbi  2160  ceqsalg  2828  eqvincg  2927  ddifstab  3336  csbprc  3537  undif4  3554  eqifdc  3639  ifnebibdc  3648  ssprsseq  3830  sssnm  3832  sneqbg  3841  opthpr  3850  elpwuni  4055  ss1o0el1  4281  exmid01  4282  exmidundif  4290  eusv2i  4546  reusv3  4551  iunpw  4571  suc11g  4649  reldmm  4942  ssxpbm  5164  ssxp1  5165  ssxp2  5166  xp11m  5167  2elresin  5434  mpteqb  5727  f1fveq  5902  f1elima  5903  f1imass  5904  fliftf  5929  nnsucuniel  6649  iserd  6714  ecopovtrn  6787  ecopover  6788  ecopovtrng  6790  ecopoverg  6791  map0g  6843  fopwdom  7005  f1finf1o  7125  mkvprop  7336  addcanpig  7532  mulcanpig  7533  srpospr  7981  readdcan  8297  cnegexlem1  8332  addcan  8337  addcan2  8338  neg11  8408  negreb  8422  add20  8632  cru  8760  mulcanapd  8819  uz11  9757  eqreznegel  9821  lbzbi  9823  xneg11  10042  xnn0xadd0  10075  xsubge0  10089  elioc2  10144  elico2  10145  elicc2  10146  fzopth  10269  2ffzeq  10349  flqidz  10518  addmodlteq  10632  frec2uzrand  10639  nninfinf  10677  expcan  10950  nn0opthd  10956  fz1eqb  11024  wrdnval  11115  eqwrd  11125  ccatalpha  11161  wrdl1s1  11178  ccatopth  11264  ccatopth2  11265  cj11  11432  sqrt0  11531  recan  11636  0dvds  12338  dvds1  12380  alzdvds  12381  nn0enne  12429  nn0oddm1d2  12436  nnoddm1d2  12437  divalgmod  12454  gcdeq0  12514  algcvgblem  12587  prmexpb  12689  4sqexercise2  12938  4sqlemsdc  12939  4sqlem11  12940  ennnfonelemim  13011  grprcan  13586  grplcan  13611  grpinv11  13618  isnzr2  14164  znidomb  14638  tgdom  14762  en1top  14767  hmeocnvb  15008  metrest  15196  perfect  15691  lgsne0  15733  2lgs  15799  2lgsoddprmlem3  15806  wrdupgren  15912  wrdumgren  15922  usgrausgrben  15986  upgriswlkdc  16106  bj-nnbist  16191  bj-nnbidc  16204  bj-peano4  16401  bj-nn0sucALT  16424