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  5606  f1ocnv2d  6050  1stconst  6197  2ndconst  6198  cnvf1o  6201  ersymb  6523  swoer  6537  erth  6553  enen1  6814  enen2  6815  domen1  6816  domen2  6817  xpmapenlem  6823  fidifsnen  6844  fundmfibi  6912  f1dmvrnfibi  6917  ordiso2  7008  omniwomnimkv  7139  enwomnilem  7141  infregelbex  9544  fzsplit2  9993  fseq1p1m1  10037  elfz2nn0  10055  btwnzge0  10243  modqsubdir  10336  zesq  10581  hashprg  10730  rereb  10814  abslt  11039  absle  11040  maxleastb  11165  maxltsup  11169  xrltmaxsup  11207  xrmaxltsup  11208  iserex  11289  mptfzshft  11392  fsumrev  11393  fprodrev  11569  dvdsadd2b  11789  nn0ob  11854  dfgcd3  11952  dfgcd2  11956  dvdsmulgcd  11967  lcmgcdeq  12024  isprm5  12083  qden1elz  12146  mhmf1o  12679  cncnp  12945  xmetxpbl  13223  dedekindicc  13326  coseq0q4123  13470  coseq0negpitopi  13472  relogeftb  13501  relogbcxpbap  13598  pwf1oexmid  13954  isomninnlem  13984  apdiff  14002  iswomninnlem  14003  ismkvnnlem  14006  redcwlpolemeq1  14008