Theorem impbida 528

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

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  eqrdav  2039  funfvbrb  5280  f1ocnv2d  5704  1stconst  5842  2ndconst  5843  cnvf1o  5846  ersymb  6120  swoer  6134  erth  6150  enen1  6311  enen2  6312  domen1  6313  domen2  6314  fidifsnen  6331  ordiso2  6357  fzsplit2  8914  fseq1p1m1  8956  elfz2nn0  8973  btwnzge0  9142  zesq  9367  rereb  9463  abslt  9684  absle  9685  iiserex  9859