Theorem impbida 604

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  622  eqrdav  2237  funfvbrb  5813  f1ocnv2d  6284  f1o3d  6288  funimass4f  6349  1stconst  6447  2ndconst  6448  cnvf1o  6451  ersymb  6811  swoer  6825  erth  6843  pw2f1odclem  7124  enen1  7130  enen2  7131  domen1  7132  domen2  7133  xpmapenlem  7139  fidifsnen  7162  fundmfibi  7242  f1dmvrnfibi  7248  2omap  7308  2omapfi  7310  ordiso2  7365  omniwomnimkv  7497  enwomnilem  7499  nninfwlpoimlemginf  7506  pw1if  7574  exmidapne  7616  infregelbex  9977  fzsplit2  10433  fzsplit3  10436  fseq1p1m1  10479  elfz2nn0  10497  infssfzcldc  10647  infssfzledc  10648  btwnzge0  10713  modqsubdir  10808  zesq  11074  hashprg  11227  sseqn  11257  hashfibclem  11260  rereb  11606  abslt  11832  absle  11833  maxleastb  11958  maxltsup  11962  xrltmaxsup  12001  xrmaxltsup  12002  iserex  12083  mptfzshft  12187  fsumrev  12188  fprodrev  12364  dvdsadd2b  12585  nn0ob  12653  bitsfzo  12700  dfgcd3  12765  dfgcd2  12769  dvdsmulgcd  12780  lcmgcdeq  12839  isprm5  12898  qden1elz  12961  ballotfilemsf1o  13235  issubmnd  13732  mhmf1o  13754  subsubm  13767  resmhm2b  13773  grpinvid1  13834  grpinvid2  13835  subsubg  13977  ssnmz  13991  ghmf1  14053  kerf1ghm  14054  ghmf1o  14055  conjnmzb  14060  0unit  14409  rhmf1o  14448  subsubrng  14495  subrgunit  14520  subsubrg  14526  ringunitap  14566  drngunitap  14581  islss3  14688  islss4  14691  lspsnel6  14717  lspsneq0b  14736  dflidl2rng  14790  cncnp  15254  xmetxpbl  15532  dedekindicc  15657  coseq0q4123  15858  coseq0negpitopi  15860  relogeftb  15889  relogbcxpbap  15990  upgr2wlkdc  16532  pw1map  16939  pwf1oexmid  16943  isomninnlem  16984  apdiff  17002  iswomninnlem  17004  ismkvnnlem  17007  redcwlpolemeq1  17009