Metamath Proof Explorer


Theorem anabsi7

Description: Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996) (Proof shortened by Wolf Lammen, 18-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 anabsi7.1 ψφψχ
2 1 anabsi6 ψφχ
3 2 ancoms φψχ