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  6773  iserd  6838  ecopovtrn  6911  ecopover  6912  ecopovtrng  6914  ecopoverg  6915  mapfset  6950  map0g  6974  fopwdom  7142  f1finf1o  7271  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  9960  eqreznegel  10029  lbzbi  10031  xneg11  10252  xnn0xadd0  10285  xsubge0  10299  elioc2  10354  elico2  10355  elicc2  10356  fzopth  10483  2ffzeq  10564  flqidz  10741  addmodlteq  10855  frec2uzrand  10862  nninfinf  10900  resq01  11115  expcan  11175  nn0opthd  11181  fz1eqb  11250  wrdnval  11356  eqwrd  11366  ccatalpha  11402  wrdl1s1  11419  ccatopth  11509  ccatopth2  11510  sq01  11681  cj11  11692  sqrt0  11791  recan  11897  0dvds  12602  dvds1  12644  alzdvds  12645  nn0enne  12693  nn0oddm1d2  12700  nnoddm1d2  12701  divalgmod  12718  gcdeq0  12778  algcvgblem  12851  prmexpb  12954  4sqexercise2  13206  4sqlemsdc  13207  4sqlem11  13208  ennnfonelemim  13372  grprcan  13900  grplcan  13925  grpinv11  13932  isnzr2  14599  znidomb  15101  tgdom  15315  en1top  15320  hmeocnvb  15561  metrest  15749  pellexlem3  16248  perfect  16318  lgsne0  16379  2lgs  16445  2lgsoddprmlem3  16452  wrdupgren  16559  wrdumgren  16569  usgrausgrben  16635  upgriswlkdc  16823  bj-nnbist  16994  bj-nnbidc  17007  bj-peano4  17203  bj-nn0sucALT  17226