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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biadanid  622  eqrdav  2237  funfvbrb  5825  f1ocnv2d  6297  f1o3d  6301  funimass4f  6363  1stconst  6461  2ndconst  6462  cnvf1o  6465  ersymb  6826  swoer  6840  erth  6858  pw2f1odclem  7140  enen1  7146  enen2  7147  domen1  7148  domen2  7149  xpmapenlem  7155  fidifsnen  7178  fundmfibi  7258  f1dmvrnfibi  7264  funisfsuppdc  7298  2omap  7324  2omapfi  7326  ordiso2  7381  omniwomnimkv  7513  enwomnilem  7515  nninfwlpoimlemginf  7522  pw1if  7590  exmidapne  7632  infregelbex  10013  fzsplit2  10471  fzsplit3  10474  fseq1p1m1  10517  elfz2nn0  10535  infssfzcldc  10685  infssfzledc  10686  btwnzge0  10755  modqsubdir  10850  zesq  11116  hashprg  11270  sseqn  11300  hashfibclem  11303  rereb  11649  abslt  11876  absle  11877  maxleastb  12002  maxltsup  12006  xrltmaxsup  12047  xrmaxltsup  12048  iserex  12129  mptfzshft  12233  fsumrev  12234  fprodrev  12410  dvdsadd2b  12631  nn0ob  12699  bitsfzo  12746  dfgcd3  12811  dfgcd2  12815  dvdsmulgcd  12826  lcmgcdeq  12885  isprm5  12945  nnmaxpwlemparts  12976  qden1elz  13009  ballotfilemsf1o  13314  issubmnd  13813  mhmf1o  13835  subsubm  13848  resmhm2b  13854  grpinvid1  13915  grpinvid2  13916  subsubg  14058  ssnmz  14072  ghmf1  14134  kerf1ghm  14135  ghmf1o  14136  conjnmzb  14141  0unit  14544  rhmf1o  14583  subsubrng  14630  subrgunit  14655  subsubrg  14661  ringunitap  14701  drngunitap  14716  islss3  14824  islss4  14827  ellspsn6  14853  lspsneq0b  14872  dflidl2rng  14926  issubassa  15121  issubassa2  15143  psrbaglefifi  15175  gsumbagdiagfi  15185  cncnp  15473  xmetxpbl  15751  dedekindicc  15876  coseq0q4123  16078  coseq0negpitopi  16080  relogeftb  16111  relogbcxpbap  16218  upgr2wlkdc  16840  pw1map  17247  pwf1oexmid  17251  isomninnlem  17302  apdiff  17321  iswomninnlem  17323  ismkvnnlem  17326  redcwlpolemeq1  17328