Theorem impbida 585

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  2138  funfvbrb  5533  f1ocnv2d  5974  1stconst  6118  2ndconst  6119  cnvf1o  6122  ersymb  6443  swoer  6457  erth  6473  enen1  6734  enen2  6735  domen1  6736  domen2  6737  xpmapenlem  6743  fidifsnen  6764  fundmfibi  6827  f1dmvrnfibi  6832  ordiso2  6920  fzsplit2  9830  fseq1p1m1  9874  elfz2nn0  9892  btwnzge0  10073  modqsubdir  10166  zesq  10410  hashprg  10554  rereb  10635  abslt  10860  absle  10861  maxleastb  10986  maxltsup  10990  xrltmaxsup  11026  xrmaxltsup  11027  iserex  11108  mptfzshft  11211  fsumrev  11212  dvdsadd2b  11540  nn0ob  11605  dfgcd3  11698  dfgcd2  11702  dvdsmulgcd  11713  lcmgcdeq  11764  qden1elz  11883  cncnp  12399  xmetxpbl  12677  dedekindicc  12780  coseq0q4123  12915  coseq0negpitopi  12917  pwf1oexmid  13194  isomninnlem  13225