Theorem impbida 596

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  614  eqrdav  2186  funfvbrb  5642  f1ocnv2d  6089  1stconst  6236  2ndconst  6237  cnvf1o  6240  ersymb  6563  swoer  6577  erth  6593  enen1  6854  enen2  6855  domen1  6856  domen2  6857  xpmapenlem  6863  fidifsnen  6884  fundmfibi  6952  f1dmvrnfibi  6957  ordiso2  7048  omniwomnimkv  7179  enwomnilem  7181  nninfwlpoimlemginf  7188  exmidapne  7273  infregelbex  9612  fzsplit2  10064  fseq1p1m1  10108  elfz2nn0  10126  btwnzge0  10314  modqsubdir  10407  zesq  10653  hashprg  10802  rereb  10886  abslt  11111  absle  11112  maxleastb  11237  maxltsup  11241  xrltmaxsup  11279  xrmaxltsup  11280  iserex  11361  mptfzshft  11464  fsumrev  11465  fprodrev  11641  dvdsadd2b  11861  nn0ob  11927  dfgcd3  12025  dfgcd2  12029  dvdsmulgcd  12040  lcmgcdeq  12097  isprm5  12156  qden1elz  12219  issubmnd  12865  mhmf1o  12883  subsubm  12896  resmhm2b  12902  grpinvid1  12957  grpinvid2  12958  subsubg  13097  ssnmz  13111  ghmf1  13167  kerf1ghm  13168  ghmf1o  13169  conjnmzb  13174  0unit  13434  subsubrng  13491  subrgunit  13516  subsubrg  13522  islss3  13625  islss4  13628  lspsnel6  13654  lspsneq0b  13673  dflidl2rng  13727  cncnp  14083  xmetxpbl  14361  dedekindicc  14464  coseq0q4123  14608  coseq0negpitopi  14610  relogeftb  14639  relogbcxpbap  14736  pwf1oexmid  15103  isomninnlem  15132  apdiff  15150  iswomninnlem  15151  ismkvnnlem  15154  redcwlpolemeq1  15156