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:  biadanid  614  eqrdav  2204  funfvbrb  5695  f1ocnv2d  6152  1stconst  6309  2ndconst  6310  cnvf1o  6313  ersymb  6636  swoer  6650  erth  6668  pw2f1odclem  6933  enen1  6939  enen2  6940  domen1  6941  domen2  6942  xpmapenlem  6948  fidifsnen  6969  fundmfibi  7042  f1dmvrnfibi  7048  ordiso2  7139  omniwomnimkv  7271  enwomnilem  7273  nninfwlpoimlemginf  7280  exmidapne  7374  infregelbex  9721  fzsplit2  10174  fseq1p1m1  10218  elfz2nn0  10236  btwnzge0  10445  modqsubdir  10540  zesq  10805  hashprg  10955  rereb  11207  abslt  11432  absle  11433  maxleastb  11558  maxltsup  11562  xrltmaxsup  11601  xrmaxltsup  11602  iserex  11683  mptfzshft  11786  fsumrev  11787  fprodrev  11963  dvdsadd2b  12184  nn0ob  12252  bitsfzo  12299  dfgcd3  12364  dfgcd2  12368  dvdsmulgcd  12379  lcmgcdeq  12438  isprm5  12497  qden1elz  12560  issubmnd  13307  mhmf1o  13335  subsubm  13348  resmhm2b  13354  grpinvid1  13417  grpinvid2  13418  subsubg  13566  ssnmz  13580  ghmf1  13642  kerf1ghm  13643  ghmf1o  13644  conjnmzb  13649  0unit  13924  rhmf1o  13963  subsubrng  14009  subrgunit  14034  subsubrg  14040  islss3  14174  islss4  14177  lspsnel6  14203  lspsneq0b  14222  dflidl2rng  14276  cncnp  14735  xmetxpbl  15013  dedekindicc  15138  coseq0q4123  15339  coseq0negpitopi  15341  relogeftb  15370  relogbcxpbap  15470  2omap  15969  pwf1oexmid  15973  isomninnlem  16006  apdiff  16024  iswomninnlem  16025  ismkvnnlem  16028  redcwlpolemeq1  16030