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  916  pm5.63dc  955  pm4.83dc  960  pm5.71dc  970  19.33b2  1678  19.9t  1691  sb4b  1883  a16gb  1914  euor2  2139  eupickbi  2163  ceqsalg  2841  eqvincg  2940  ddifstab  3350  csbprc  3553  undif4  3570  eqifdc  3658  ifnebibdc  3667  ssprsseq  3855  sssnm  3857  sneqbg  3866  opthpr  3875  elpwuni  4080  ss1o0el1  4309  exmid01  4310  exmidundif  4318  eusv2i  4575  reusv3  4580  iunpw  4600  suc11g  4678  reldmm  4974  ssxpbm  5197  ssxp1  5198  ssxp2  5199  xp11m  5200  2elresin  5468  mpteqb  5767  f1fveq  5944  f1elima  5945  f1imass  5946  fliftf  5971  nnsucuniel  6727  iserd  6792  ecopovtrn  6865  ecopover  6866  ecopovtrng  6868  ecopoverg  6869  map0g  6921  fopwdom  7088  f1finf1o  7216  mkvprop  7448  addcanpig  7648  mulcanpig  7649  srpospr  8097  readdcan  8412  cnegexlem1  8447  addcan  8452  addcan2  8453  neg11  8523  negreb  8537  add20  8747  cru  8875  mulcanapd  8934  uz11  9876  eqreznegel  9945  lbzbi  9947  xneg11  10166  xnn0xadd0  10199  xsubge0  10213  elioc2  10268  elico2  10269  elicc2  10270  fzopth  10394  2ffzeq  10474  flqidz  10645  addmodlteq  10759  frec2uzrand  10766  nninfinf  10804  expcan  11077  nn0opthd  11083  fz1eqb  11151  wrdnval  11251  eqwrd  11261  ccatalpha  11297  wrdl1s1  11314  ccatopth  11404  ccatopth2  11405  cj11  11586  sqrt0  11685  recan  11790  0dvds  12493  dvds1  12535  alzdvds  12536  nn0enne  12584  nn0oddm1d2  12591  nnoddm1d2  12592  divalgmod  12609  gcdeq0  12669  algcvgblem  12742  prmexpb  12844  4sqexercise2  13093  4sqlemsdc  13094  4sqlem11  13095  ennnfonelemim  13167  grprcan  13742  grplcan  13767  grpinv11  13774  isnzr2  14321  znidomb  14798  tgdom  14929  en1top  14934  hmeocnvb  15175  metrest  15363  pellexlem3  15839  perfect  15861  lgsne0  15903  2lgs  15969  2lgsoddprmlem3  15976  wrdupgren  16083  wrdumgren  16093  usgrausgrben  16159  upgriswlkdc  16347  bj-nnbist  16508  bj-nnbidc  16521  bj-peano4  16717  bj-nn0sucALT  16740