Metamath Proof Explorer


Theorem impbida

Description: Deduce an equivalence from two implications. Variant of impbid . (Contributed by NM, 17-Feb-2007)

Ref Expression
Hypotheses impbida.1
|- ( ( ph /\ ps ) -> ch )
impbida.2
|- ( ( ph /\ ch ) -> ps )
Assertion impbida
|- ( ph -> ( ps <-> ch ) )

Proof

Step Hyp Ref Expression
1 impbida.1
 |-  ( ( ph /\ ps ) -> ch )
2 impbida.2
 |-  ( ( ph /\ ch ) -> ps )
3 1 ex
 |-  ( ph -> ( ps -> ch ) )
4 2 ex
 |-  ( ph -> ( ch -> ps ) )
5 3 4 impbid
 |-  ( ph -> ( ps <-> ch ) )