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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  impbid2  143  iba  300  ibar  301  pm4.81dc  920  pm5.63dc  959  pm4.83dc  964  pm5.71dc  974  19.33b2  1682  19.9t  1695  sb4b  1887  a16gb  1918  euor2  2145  eupickbi  2169  ceqsalg  2850  eqvincg  2950  ddifstab  3361  csbprc  3572  undif4  3587  eqifdc  3677  ifnebibdc  3686  ssprsseq  3877  sssnm  3879  sneqbg  3888  opthpr  3897  elpwuni  4102  ss1o0el1  4336  exmid01  4337  exmidundif  4345  eusv2i  4603  reusv3  4608  iunpw  4628  suc11g  4706  reldmm  5002  ssxpbm  5226  ssxp1  5227  ssxp2  5228  xp11m  5229  2elresin  5497  mpteqb  5799  f1fveq  5981  f1elima  5982  f1imass  5983  fliftf  6008  nnsucuniel  6772  iserd  6837  ecopovtrn  6910  ecopover  6911  ecopovtrng  6913  ecopoverg  6914  mapfset  6949  map0g  6973  fopwdom  7140  f1finf1o  7269  mkvprop  7504  addcanpig  7707  mulcanpig  7708  srpospr  8156  readdcan  8473  cnegexlem1  8508  addcan  8513  addcan2  8514  neg11  8584  negreb  8598  add20  8809  cru  8938  mulcanapd  8997  uz11  9961  eqreznegel  10030  lbzbi  10032  xneg11  10253  xnn0xadd0  10286  xsubge0  10300  elioc2  10355  elico2  10356  elicc2  10357  fzopth  10484  2ffzeq  10565  flqidz  10742  addmodlteq  10856  frec2uzrand  10863  nninfinf  10901  resq01  11116  expcan  11176  nn0opthd  11182  fz1eqb  11251  wrdnval  11357  eqwrd  11367  ccatalpha  11403  wrdl1s1  11420  ccatopth  11510  ccatopth2  11511  sq01  11682  cj11  11693  sqrt0  11792  recan  11898  0dvds  12603  dvds1  12645  alzdvds  12646  nn0enne  12694  nn0oddm1d2  12701  nnoddm1d2  12702  divalgmod  12719  gcdeq0  12779  algcvgblem  12852  prmexpb  12955  4sqexercise2  13207  4sqlemsdc  13208  4sqlem11  13209  ennnfonelemim  13373  grprcan  13901  grplcan  13926  grpinv11  13933  isnzr2  14600  znidomb  15102  tgdom  15298  en1top  15303  hmeocnvb  15544  metrest  15732  pellexlem3  16231  perfect  16301  lgsne0  16362  2lgs  16428  2lgsoddprmlem3  16435  wrdupgren  16542  wrdumgren  16552  usgrausgrben  16618  upgriswlkdc  16806  bj-nnbist  16977  bj-nnbidc  16990  bj-peano4  17186  bj-nn0sucALT  17209