Theorem impbida 598

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  616  eqrdav  2228  funfvbrb  5750  f1ocnv2d  6216  1stconst  6373  2ndconst  6374  cnvf1o  6377  ersymb  6702  swoer  6716  erth  6734  pw2f1odclem  7003  enen1  7009  enen2  7010  domen1  7011  domen2  7012  xpmapenlem  7018  fidifsnen  7040  fundmfibi  7116  f1dmvrnfibi  7122  ordiso2  7213  omniwomnimkv  7345  enwomnilem  7347  nninfwlpoimlemginf  7354  pw1if  7421  exmidapne  7457  infregelbex  9805  fzsplit2  10258  fseq1p1m1  10302  elfz2nn0  10320  btwnzge0  10532  modqsubdir  10627  zesq  10892  hashprg  11043  rereb  11390  abslt  11615  absle  11616  maxleastb  11741  maxltsup  11745  xrltmaxsup  11784  xrmaxltsup  11785  iserex  11866  mptfzshft  11969  fsumrev  11970  fprodrev  12146  dvdsadd2b  12367  nn0ob  12435  bitsfzo  12482  dfgcd3  12547  dfgcd2  12551  dvdsmulgcd  12562  lcmgcdeq  12621  isprm5  12680  qden1elz  12743  issubmnd  13491  mhmf1o  13519  subsubm  13532  resmhm2b  13538  grpinvid1  13601  grpinvid2  13602  subsubg  13750  ssnmz  13764  ghmf1  13826  kerf1ghm  13827  ghmf1o  13828  conjnmzb  13833  0unit  14109  rhmf1o  14148  subsubrng  14194  subrgunit  14219  subsubrg  14225  islss3  14359  islss4  14362  lspsnel6  14388  lspsneq0b  14407  dflidl2rng  14461  cncnp  14920  xmetxpbl  15198  dedekindicc  15323  coseq0q4123  15524  coseq0negpitopi  15526  relogeftb  15555  relogbcxpbap  15655  upgr2wlkdc  16121  2omap  16446  pw1map  16448  pwf1oexmid  16452  isomninnlem  16486  apdiff  16504  iswomninnlem  16505  ismkvnnlem  16508  redcwlpolemeq1  16510