Theorem impbida 596

Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)

Hypotheses

Ref	Expression
impbida.1	|- ( ( ph /\ ps ) -> ch )
impbida.2	|- ( ( ph /\ ch ) -> ps )

Assertion

Ref	Expression
impbida	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem impbida

Step	Hyp	Ref	Expression
1		impbida.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 115	. 2 |- ( ph -> ( ps -> ch ) )
3		impbida.2	. . 3 |- ( ( ph /\ ch ) -> ps )
4	3	ex 115	. 2 |- ( ph -> ( ch -> ps ) )
5	2, 4	impbid 129	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> 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:  eqrdav  2176  funfvbrb  5631  f1ocnv2d  6077  1stconst  6224  2ndconst  6225  cnvf1o  6228  ersymb  6551  swoer  6565  erth  6581  enen1  6842  enen2  6843  domen1  6844  domen2  6845  xpmapenlem  6851  fidifsnen  6872  fundmfibi  6940  f1dmvrnfibi  6945  ordiso2  7036  omniwomnimkv  7167  enwomnilem  7169  nninfwlpoimlemginf  7176  exmidapne  7261  infregelbex  9600  fzsplit2  10052  fseq1p1m1  10096  elfz2nn0  10114  btwnzge0  10302  modqsubdir  10395  zesq  10641  hashprg  10790  rereb  10874  abslt  11099  absle  11100  maxleastb  11225  maxltsup  11229  xrltmaxsup  11267  xrmaxltsup  11268  iserex  11349  mptfzshft  11452  fsumrev  11453  fprodrev  11629  dvdsadd2b  11849  nn0ob  11915  dfgcd3  12013  dfgcd2  12017  dvdsmulgcd  12028  lcmgcdeq  12085  isprm5  12144  qden1elz  12207  issubmnd  12848  mhmf1o  12866  grpinvid1  12929  grpinvid2  12930  subsubg  13062  ssnmz  13076  0unit  13303  subrgunit  13365  subsubrg  13371  islss3  13471  islss4  13474  cncnp  13769  xmetxpbl  14047  dedekindicc  14150  coseq0q4123  14294  coseq0negpitopi  14296  relogeftb  14325  relogbcxpbap  14422  pwf1oexmid  14788  isomninnlem  14817  apdiff  14835  iswomninnlem  14836  ismkvnnlem  14839  redcwlpolemeq1  14841