Theorem impbid1 141

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 128	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  iba  298  ibar  299  pm4.81dc  903  pm5.63dc  941  pm4.83dc  946  pm5.71dc  956  19.33b2  1622  19.9t  1635  sb4b  1827  a16gb  1858  euor2  2077  eupickbi  2101  ceqsalg  2758  eqvincg  2854  ddifstab  3259  csbprc  3460  undif4  3477  eqifdc  3560  sssnm  3741  sneqbg  3750  opthpr  3759  elpwuni  3962  ss1o0el1  4183  exmid01  4184  exmidundif  4192  eusv2i  4440  reusv3  4445  iunpw  4465  suc11g  4541  ssxpbm  5046  ssxp1  5047  ssxp2  5048  xp11m  5049  2elresin  5309  mpteqb  5586  f1fveq  5751  f1elima  5752  f1imass  5753  fliftf  5778  nnsucuniel  6474  iserd  6539  ecopovtrn  6610  ecopover  6611  ecopovtrng  6613  ecopoverg  6614  map0g  6666  fopwdom  6814  f1finf1o  6924  mkvprop  7134  addcanpig  7296  mulcanpig  7297  srpospr  7745  readdcan  8059  cnegexlem1  8094  addcan  8099  addcan2  8100  neg11  8170  negreb  8184  add20  8393  cru  8521  mulcanapd  8579  uz11  9509  eqreznegel  9573  lbzbi  9575  xneg11  9791  xnn0xadd0  9824  xsubge0  9838  elioc2  9893  elico2  9894  elicc2  9895  fzopth  10017  2ffzeq  10097  flqidz  10242  addmodlteq  10354  frec2uzrand  10361  expcan  10650  nn0opthd  10656  fz1eqb  10725  cj11  10869  sqrt0  10968  recan  11073  0dvds  11773  dvds1  11813  alzdvds  11814  nn0enne  11861  nn0oddm1d2  11868  nnoddm1d2  11869  divalgmod  11886  gcdeq0  11932  algcvgblem  12003  prmexpb  12105  ennnfonelemim  12379  grprcan  12740  grplcan  12761  grpinv11  12768  tgdom  12866  en1top  12871  hmeocnvb  13112  metrest  13300  lgsne0  13733  bj-nnbist  13779  bj-nnbidc  13792  bj-peano4  13990  bj-nn0sucALT  14013