Metamath Proof Explorer

Theorem biimp3ar

Description: Infer implication from a logical equivalence. Similar to biimpar . (Contributed by NM, 2-Jan-2009)

Ref Expression
Hypothesis biimp3a.1 
|- ( ( ph /\ ps ) -> ( ch <-> th ) )
Assertion biimp3ar 
|- ( ( ph /\ ps /\ th ) -> ch )

Proof

Step Hyp Ref Expression
1 biimp3a.1 
 |-  ( ( ph /\ ps ) -> ( ch <-> th ) )
2 1 exbiri 
 |-  ( ph -> ( ps -> ( th -> ch ) ) )
3 2 3imp 
 |-  ( ( ph /\ ps /\ th ) -> ch )