Theorem impbida 586

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 114	. 2 |- ( ph -> ( ps -> ch ) )
3		impbida.2	. . 3 |- ( ( ph /\ ch ) -> ps )
4	3	ex 114	. 2 |- ( ph -> ( ch -> ps ) )
5	2, 4	impbid 128	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> 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:  eqrdav  2164  funfvbrb  5597  f1ocnv2d  6041  1stconst  6185  2ndconst  6186  cnvf1o  6189  ersymb  6511  swoer  6525  erth  6541  enen1  6802  enen2  6803  domen1  6804  domen2  6805  xpmapenlem  6811  fidifsnen  6832  fundmfibi  6900  f1dmvrnfibi  6905  ordiso2  6996  omniwomnimkv  7127  enwomnilem  7129  infregelbex  9532  fzsplit2  9981  fseq1p1m1  10025  elfz2nn0  10043  btwnzge0  10231  modqsubdir  10324  zesq  10569  hashprg  10717  rereb  10801  abslt  11026  absle  11027  maxleastb  11152  maxltsup  11156  xrltmaxsup  11194  xrmaxltsup  11195  iserex  11276  mptfzshft  11379  fsumrev  11380  fprodrev  11556  dvdsadd2b  11776  nn0ob  11841  dfgcd3  11939  dfgcd2  11943  dvdsmulgcd  11954  lcmgcdeq  12011  isprm5  12070  qden1elz  12133  cncnp  12830  xmetxpbl  13108  dedekindicc  13211  coseq0q4123  13355  coseq0negpitopi  13357  relogeftb  13386  relogbcxpbap  13483  pwf1oexmid  13839  isomninnlem  13869  apdiff  13887  iswomninnlem  13888  ismkvnnlem  13891  redcwlpolemeq1  13893