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  5748  f1ocnv2d  6210  1stconst  6367  2ndconst  6368  cnvf1o  6371  ersymb  6694  swoer  6708  erth  6726  pw2f1odclem  6995  enen1  7001  enen2  7002  domen1  7003  domen2  7004  xpmapenlem  7010  fidifsnen  7032  fundmfibi  7105  f1dmvrnfibi  7111  ordiso2  7202  omniwomnimkv  7334  enwomnilem  7336  nninfwlpoimlemginf  7343  pw1if  7410  exmidapne  7446  infregelbex  9793  fzsplit2  10246  fseq1p1m1  10290  elfz2nn0  10308  btwnzge0  10520  modqsubdir  10615  zesq  10880  hashprg  11030  rereb  11374  abslt  11599  absle  11600  maxleastb  11725  maxltsup  11729  xrltmaxsup  11768  xrmaxltsup  11769  iserex  11850  mptfzshft  11953  fsumrev  11954  fprodrev  12130  dvdsadd2b  12351  nn0ob  12419  bitsfzo  12466  dfgcd3  12531  dfgcd2  12535  dvdsmulgcd  12546  lcmgcdeq  12605  isprm5  12664  qden1elz  12727  issubmnd  13475  mhmf1o  13503  subsubm  13516  resmhm2b  13522  grpinvid1  13585  grpinvid2  13586  subsubg  13734  ssnmz  13748  ghmf1  13810  kerf1ghm  13811  ghmf1o  13812  conjnmzb  13817  0unit  14093  rhmf1o  14132  subsubrng  14178  subrgunit  14203  subsubrg  14209  islss3  14343  islss4  14346  lspsnel6  14372  lspsneq0b  14391  dflidl2rng  14445  cncnp  14904  xmetxpbl  15182  dedekindicc  15307  coseq0q4123  15508  coseq0negpitopi  15510  relogeftb  15539  relogbcxpbap  15639  2omap  16359  pw1map  16361  pwf1oexmid  16365  isomninnlem  16398  apdiff  16416  iswomninnlem  16417  ismkvnnlem  16420  redcwlpolemeq1  16422