Metamath Proof Explorer


Theorem ancoms

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

Ref Expression
Hypothesis ancoms.1 φψχ
Assertion ancoms ψφχ

Proof

Step Hyp Ref Expression
1 ancoms.1 φψχ
2 1 expcom ψφχ
3 2 imp ψφχ