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  lspsnel6  13499  lspsneq0b  13518  cncnp  13815  xmetxpbl  14093  dedekindicc  14196  coseq0q4123  14340  coseq0negpitopi  14342  relogeftb  14371  relogbcxpbap  14468  pwf1oexmid  14834  isomninnlem  14863  apdiff  14881  iswomninnlem  14882  ismkvnnlem  14885  redcwlpolemeq1  14887