Theorem impbida 600

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  618  eqrdav  2230  funfvbrb  5760  f1ocnv2d  6227  1stconst  6386  2ndconst  6387  cnvf1o  6390  ersymb  6716  swoer  6730  erth  6748  pw2f1odclem  7020  enen1  7026  enen2  7027  domen1  7028  domen2  7029  xpmapenlem  7035  fidifsnen  7057  fundmfibi  7137  f1dmvrnfibi  7143  ordiso2  7234  omniwomnimkv  7366  enwomnilem  7368  nninfwlpoimlemginf  7375  pw1if  7443  exmidapne  7479  infregelbex  9832  fzsplit2  10285  fseq1p1m1  10329  elfz2nn0  10347  btwnzge0  10561  modqsubdir  10656  zesq  10921  hashprg  11073  rereb  11441  abslt  11666  absle  11667  maxleastb  11792  maxltsup  11796  xrltmaxsup  11835  xrmaxltsup  11836  iserex  11917  mptfzshft  12021  fsumrev  12022  fprodrev  12198  dvdsadd2b  12419  nn0ob  12487  bitsfzo  12534  dfgcd3  12599  dfgcd2  12603  dvdsmulgcd  12614  lcmgcdeq  12673  isprm5  12732  qden1elz  12795  issubmnd  13543  mhmf1o  13571  subsubm  13584  resmhm2b  13590  grpinvid1  13653  grpinvid2  13654  subsubg  13802  ssnmz  13816  ghmf1  13878  kerf1ghm  13879  ghmf1o  13880  conjnmzb  13885  0unit  14162  rhmf1o  14201  subsubrng  14247  subrgunit  14272  subsubrg  14278  islss3  14412  islss4  14415  lspsnel6  14441  lspsneq0b  14460  dflidl2rng  14514  cncnp  14973  xmetxpbl  15251  dedekindicc  15376  coseq0q4123  15577  coseq0negpitopi  15579  relogeftb  15608  relogbcxpbap  15708  upgr2wlkdc  16247  2omap  16645  pw1map  16647  pwf1oexmid  16651  isomninnlem  16685  apdiff  16703  iswomninnlem  16705  ismkvnnlem  16708  redcwlpolemeq1  16710