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  2233  funfvbrb  5796  f1ocnv2d  6267  f1o3d  6271  funimass4f  6332  1stconst  6430  2ndconst  6431  cnvf1o  6434  ersymb  6794  swoer  6808  erth  6826  pw2f1odclem  7100  enen1  7106  enen2  7107  domen1  7108  domen2  7109  xpmapenlem  7115  fidifsnen  7138  fundmfibi  7218  f1dmvrnfibi  7224  2omap  7282  2omapfi  7284  ordiso2  7339  omniwomnimkv  7471  enwomnilem  7473  nninfwlpoimlemginf  7480  pw1if  7548  exmidapne  7590  infregelbex  9948  fzsplit2  10404  fzsplit3  10407  fseq1p1m1  10450  elfz2nn0  10468  infssfzcldc  10618  infssfzledc  10619  btwnzge0  10684  modqsubdir  10779  zesq  11045  hashprg  11198  sseqn  11228  hashfibclem  11231  rereb  11573  abslt  11798  absle  11799  maxleastb  11924  maxltsup  11928  xrltmaxsup  11967  xrmaxltsup  11968  iserex  12049  mptfzshft  12153  fsumrev  12154  fprodrev  12330  dvdsadd2b  12551  nn0ob  12619  bitsfzo  12666  dfgcd3  12731  dfgcd2  12735  dvdsmulgcd  12746  lcmgcdeq  12805  isprm5  12864  qden1elz  12927  ballotfilemsf1o  13201  issubmnd  13703  mhmf1o  13725  subsubm  13738  resmhm2b  13744  grpinvid1  13807  grpinvid2  13808  subsubg  13950  ssnmz  13964  ghmf1  14026  kerf1ghm  14027  ghmf1o  14028  conjnmzb  14033  0unit  14374  rhmf1o  14413  subsubrng  14460  subrgunit  14485  subsubrg  14491  ringunitap  14531  drngunitap  14546  islss3  14653  islss4  14656  lspsnel6  14682  lspsneq0b  14701  dflidl2rng  14755  cncnp  15221  xmetxpbl  15499  dedekindicc  15624  coseq0q4123  15825  coseq0negpitopi  15827  relogeftb  15856  relogbcxpbap  15956  upgr2wlkdc  16498  pw1map  16895  pwf1oexmid  16899  isomninnlem  16940  apdiff  16958  iswomninnlem  16960  ismkvnnlem  16963  redcwlpolemeq1  16965