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  5822  f1ocnv2d  6294  f1o3d  6298  funimass4f  6359  1stconst  6457  2ndconst  6458  cnvf1o  6461  ersymb  6821  swoer  6835  erth  6853  pw2f1odclem  7134  enen1  7140  enen2  7141  domen1  7142  domen2  7143  xpmapenlem  7149  fidifsnen  7172  fundmfibi  7252  f1dmvrnfibi  7258  2omap  7318  2omapfi  7320  ordiso2  7375  omniwomnimkv  7507  enwomnilem  7509  nninfwlpoimlemginf  7516  pw1if  7584  exmidapne  7626  infregelbex  9998  fzsplit2  10455  fzsplit3  10458  fseq1p1m1  10501  elfz2nn0  10519  infssfzcldc  10669  infssfzledc  10670  btwnzge0  10735  modqsubdir  10830  zesq  11096  hashprg  11249  sseqn  11279  hashfibclem  11282  rereb  11628  abslt  11854  absle  11855  maxleastb  11980  maxltsup  11984  xrltmaxsup  12023  xrmaxltsup  12024  iserex  12105  mptfzshft  12209  fsumrev  12210  fprodrev  12386  dvdsadd2b  12607  nn0ob  12675  bitsfzo  12722  dfgcd3  12787  dfgcd2  12791  dvdsmulgcd  12802  lcmgcdeq  12861  isprm5  12920  qden1elz  12983  ballotfilemsf1o  13257  issubmnd  13755  mhmf1o  13777  subsubm  13790  resmhm2b  13796  grpinvid1  13857  grpinvid2  13858  subsubg  14000  ssnmz  14014  ghmf1  14076  kerf1ghm  14077  ghmf1o  14078  conjnmzb  14083  0unit  14436  rhmf1o  14475  subsubrng  14522  subrgunit  14547  subsubrg  14553  ringunitap  14593  drngunitap  14608  islss3  14716  islss4  14719  ellspsn6  14745  lspsneq0b  14764  dflidl2rng  14818  issubassa  15013  issubassa2  15035  cncnp  15331  xmetxpbl  15609  dedekindicc  15734  coseq0q4123  15935  coseq0negpitopi  15937  relogeftb  15966  relogbcxpbap  16067  upgr2wlkdc  16618  pw1map  17025  pwf1oexmid  17029  isomninnlem  17079  apdiff  17097  iswomninnlem  17099  ismkvnnlem  17102  redcwlpolemeq1  17104