Metamath Proof Explorer


Theorem 3anrev

Description: Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994)

Ref Expression
Assertion 3anrev φψχχψφ

Proof

Step Hyp Ref Expression
1 3ancoma φψχψφχ
2 3anrot χψφψφχ
3 1 2 bitr4i φψχχψφ