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  4334  exmid01  4335  exmidundif  4343  eusv2i  4601  reusv3  4606  iunpw  4626  suc11g  4704  reldmm  5000  ssxpbm  5223  ssxp1  5224  ssxp2  5225  xp11m  5226  2elresin  5494  mpteqb  5796  f1fveq  5978  f1elima  5979  f1imass  5980  fliftf  6005  nnsucuniel  6768  iserd  6833  ecopovtrn  6906  ecopover  6907  ecopovtrng  6909  ecopoverg  6910  mapfset  6945  map0g  6969  fopwdom  7136  f1finf1o  7264  mkvprop  7498  addcanpig  7701  mulcanpig  7702  srpospr  8150  readdcan  8466  cnegexlem1  8501  addcan  8506  addcan2  8507  neg11  8577  negreb  8591  add20  8802  cru  8930  mulcanapd  8989  uz11  9945  eqreznegel  10014  lbzbi  10016  xneg11  10236  xnn0xadd0  10269  xsubge0  10283  elioc2  10338  elico2  10339  elicc2  10340  fzopth  10467  2ffzeq  10548  flqidz  10721  addmodlteq  10835  frec2uzrand  10842  nninfinf  10880  resq01  11095  expcan  11154  nn0opthd  11160  fz1eqb  11229  wrdnval  11335  eqwrd  11345  ccatalpha  11381  wrdl1s1  11398  ccatopth  11488  ccatopth2  11489  sq01  11660  cj11  11671  sqrt0  11770  recan  11875  0dvds  12578  dvds1  12620  alzdvds  12621  nn0enne  12669  nn0oddm1d2  12676  nnoddm1d2  12677  divalgmod  12694  gcdeq0  12754  algcvgblem  12827  prmexpb  12929  4sqexercise2  13178  4sqlemsdc  13179  4sqlem11  13180  ennnfonelemim  13315  grprcan  13842  grplcan  13867  grpinv11  13874  isnzr2  14491  znidomb  14993  tgdom  15173  en1top  15178  hmeocnvb  15419  metrest  15607  pellexlem3  16093  perfect  16115  lgsne0  16157  2lgs  16223  2lgsoddprmlem3  16230  wrdupgren  16337  wrdumgren  16347  usgrausgrben  16413  upgriswlkdc  16601  bj-nnbist  16772  bj-nnbidc  16785  bj-peano4  16981  bj-nn0sucALT  17004