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  908  pm5.63dc  946  pm4.83dc  951  pm5.71dc  961  19.33b2  1629  19.9t  1642  sb4b  1834  a16gb  1865  euor2  2084  eupickbi  2108  ceqsalg  2765  eqvincg  2861  ddifstab  3267  csbprc  3468  undif4  3485  eqifdc  3568  sssnm  3752  sneqbg  3761  opthpr  3770  elpwuni  3973  ss1o0el1  4194  exmid01  4195  exmidundif  4203  eusv2i  4452  reusv3  4457  iunpw  4477  suc11g  4553  ssxpbm  5060  ssxp1  5061  ssxp2  5062  xp11m  5063  2elresin  5323  mpteqb  5602  f1fveq  5767  f1elima  5768  f1imass  5769  fliftf  5794  nnsucuniel  6490  iserd  6555  ecopovtrn  6626  ecopover  6627  ecopovtrng  6629  ecopoverg  6630  map0g  6682  fopwdom  6830  f1finf1o  6940  mkvprop  7150  addcanpig  7321  mulcanpig  7322  srpospr  7770  readdcan  8084  cnegexlem1  8119  addcan  8124  addcan2  8125  neg11  8195  negreb  8209  add20  8418  cru  8546  mulcanapd  8604  uz11  9536  eqreznegel  9600  lbzbi  9602  xneg11  9818  xnn0xadd0  9851  xsubge0  9865  elioc2  9920  elico2  9921  elicc2  9922  fzopth  10044  2ffzeq  10124  flqidz  10269  addmodlteq  10381  frec2uzrand  10388  expcan  10677  nn0opthd  10683  fz1eqb  10751  cj11  10895  sqrt0  10994  recan  11099  0dvds  11799  dvds1  11839  alzdvds  11840  nn0enne  11887  nn0oddm1d2  11894  nnoddm1d2  11895  divalgmod  11912  gcdeq0  11958  algcvgblem  12029  prmexpb  12131  ennnfonelemim  12405  grprcan  12797  grplcan  12818  grpinv11  12825  tgdom  13232  en1top  13237  hmeocnvb  13478  metrest  13666  lgsne0  14099  bj-nnbist  14145  bj-nnbidc  14158  bj-peano4  14356  bj-nn0sucALT  14379