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  2141  eupickbi  2165  ceqsalg  2844  eqvincg  2943  ddifstab  3353  csbprc  3556  undif4  3573  eqifdc  3661  ifnebibdc  3670  ssprsseq  3858  sssnm  3860  sneqbg  3869  opthpr  3878  elpwuni  4083  ss1o0el1  4312  exmid01  4313  exmidundif  4321  eusv2i  4578  reusv3  4583  iunpw  4603  suc11g  4681  reldmm  4977  ssxpbm  5200  ssxp1  5201  ssxp2  5202  xp11m  5203  2elresin  5471  mpteqb  5770  f1fveq  5947  f1elima  5948  f1imass  5949  fliftf  5974  nnsucuniel  6730  iserd  6795  ecopovtrn  6868  ecopover  6869  ecopovtrng  6871  ecopoverg  6872  map0g  6924  fopwdom  7091  f1finf1o  7219  mkvprop  7451  addcanpig  7651  mulcanpig  7652  srpospr  8100  readdcan  8415  cnegexlem1  8450  addcan  8455  addcan2  8456  neg11  8526  negreb  8540  add20  8750  cru  8878  mulcanapd  8937  uz11  9880  eqreznegel  9949  lbzbi  9951  xneg11  10170  xnn0xadd0  10203  xsubge0  10217  elioc2  10272  elico2  10273  elicc2  10274  fzopth  10398  2ffzeq  10479  flqidz  10650  addmodlteq  10764  frec2uzrand  10771  nninfinf  10809  expcan  11082  nn0opthd  11088  fz1eqb  11157  wrdnval  11259  eqwrd  11269  ccatalpha  11305  wrdl1s1  11322  ccatopth  11412  ccatopth2  11413  cj11  11594  sqrt0  11693  recan  11798  0dvds  12501  dvds1  12543  alzdvds  12544  nn0enne  12592  nn0oddm1d2  12599  nnoddm1d2  12600  divalgmod  12617  gcdeq0  12677  algcvgblem  12750  prmexpb  12852  4sqexercise2  13101  4sqlemsdc  13102  4sqlem11  13103  ennnfonelemim  13192  grprcan  13767  grplcan  13792  grpinv11  13799  isnzr2  14346  znidomb  14823  tgdom  14954  en1top  14959  hmeocnvb  15200  metrest  15388  pellexlem3  15864  perfect  15886  lgsne0  15928  2lgs  15994  2lgsoddprmlem3  16001  wrdupgren  16108  wrdumgren  16118  usgrausgrben  16184  upgriswlkdc  16372  bj-nnbist  16533  bj-nnbidc  16546  bj-peano4  16742  bj-nn0sucALT  16765