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  909  pm5.63dc  948  pm4.83dc  953  pm5.71dc  963  19.33b2  1640  19.9t  1653  sb4b  1845  a16gb  1876  euor2  2096  eupickbi  2120  ceqsalg  2780  eqvincg  2876  ddifstab  3282  csbprc  3483  undif4  3500  eqifdc  3584  sssnm  3769  sneqbg  3778  opthpr  3787  elpwuni  3991  ss1o0el1  4215  exmid01  4216  exmidundif  4224  eusv2i  4473  reusv3  4478  iunpw  4498  suc11g  4574  ssxpbm  5082  ssxp1  5083  ssxp2  5084  xp11m  5085  2elresin  5346  mpteqb  5627  f1fveq  5794  f1elima  5795  f1imass  5796  fliftf  5821  nnsucuniel  6521  iserd  6586  ecopovtrn  6659  ecopover  6660  ecopovtrng  6662  ecopoverg  6663  map0g  6715  fopwdom  6865  f1finf1o  6977  mkvprop  7187  addcanpig  7364  mulcanpig  7365  srpospr  7813  readdcan  8128  cnegexlem1  8163  addcan  8168  addcan2  8169  neg11  8239  negreb  8253  add20  8462  cru  8590  mulcanapd  8649  uz11  9582  eqreznegel  9646  lbzbi  9648  xneg11  9866  xnn0xadd0  9899  xsubge0  9913  elioc2  9968  elico2  9969  elicc2  9970  fzopth  10093  2ffzeq  10173  flqidz  10319  addmodlteq  10431  frec2uzrand  10438  expcan  10731  nn0opthd  10737  fz1eqb  10805  cj11  10949  sqrt0  11048  recan  11153  0dvds  11853  dvds1  11894  alzdvds  11895  nn0enne  11942  nn0oddm1d2  11949  nnoddm1d2  11950  divalgmod  11967  gcdeq0  12013  algcvgblem  12084  prmexpb  12186  4sqexercise2  12434  4sqlemsdc  12435  4sqlem11  12436  ennnfonelemim  12478  grprcan  12996  grplcan  13021  grpinv11  13028  tgdom  14049  en1top  14054  hmeocnvb  14295  metrest  14483  lgsne0  14917  2lgsoddprmlem3  14937  bj-nnbist  14974  bj-nnbidc  14987  bj-peano4  15185  bj-nn0sucALT  15208