Metamath Proof Explorer

Theorem ancoms

Description: Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994)

Ref Expression
Hypothesis ancoms.1 
|- ( ( ph /\ ps ) -> ch )
Assertion ancoms 
|- ( ( ps /\ ph ) -> ch )

Proof

Step Hyp Ref Expression
1 ancoms.1 
 |-  ( ( ph /\ ps ) -> ch )
2 1 expcom 
 |-  ( ps -> ( ph -> ch ) )
3 2 imp 
 |-  ( ( ps /\ ph ) -> ch )