Metamath Proof Explorer

Theorem simplbi2comt

Description: Closed form of simplbi2com . (Contributed by Alan Sare, 22-Jul-2012)

Ref Expression
Assertion simplbi2comt 
|- ( ( ph <-> ( ps /\ ch ) ) -> ( ch -> ( ps -> ph ) ) )

Proof

Step Hyp Ref Expression
1 biimpr 
 |-  ( ( ph <-> ( ps /\ ch ) ) -> ( ( ps /\ ch ) -> ph ) )
2 1 expcomd 
 |-  ( ( ph <-> ( ps /\ ch ) ) -> ( ch -> ( ps -> ph ) ) )