Theorem impbida 591

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 114	. 2 |- ( ph -> ( ps -> ch ) )
3		impbida.2	. . 3 |- ( ( ph /\ ch ) -> ps )
4	3	ex 114	. 2 |- ( ph -> ( ch -> ps ) )
5	2, 4	impbid 128	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eqrdav  2169  funfvbrb  5609  f1ocnv2d  6053  1stconst  6200  2ndconst  6201  cnvf1o  6204  ersymb  6527  swoer  6541  erth  6557  enen1  6818  enen2  6819  domen1  6820  domen2  6821  xpmapenlem  6827  fidifsnen  6848  fundmfibi  6916  f1dmvrnfibi  6921  ordiso2  7012  omniwomnimkv  7143  enwomnilem  7145  nninfwlpoimlemginf  7152  infregelbex  9557  fzsplit2  10006  fseq1p1m1  10050  elfz2nn0  10068  btwnzge0  10256  modqsubdir  10349  zesq  10594  hashprg  10743  rereb  10827  abslt  11052  absle  11053  maxleastb  11178  maxltsup  11182  xrltmaxsup  11220  xrmaxltsup  11221  iserex  11302  mptfzshft  11405  fsumrev  11406  fprodrev  11582  dvdsadd2b  11802  nn0ob  11867  dfgcd3  11965  dfgcd2  11969  dvdsmulgcd  11980  lcmgcdeq  12037  isprm5  12096  qden1elz  12159  mhmf1o  12693  grpinvid1  12754  grpinvid2  12755  cncnp  13024  xmetxpbl  13302  dedekindicc  13405  coseq0q4123  13549  coseq0negpitopi  13551  relogeftb  13580  relogbcxpbap  13677  pwf1oexmid  14032  isomninnlem  14062  apdiff  14080  iswomninnlem  14081  ismkvnnlem  14084  redcwlpolemeq1  14086