Metamath Proof Explorer


Theorem consym1

Description: A symmetry with /\ .

See negsym1 for more information. (Contributed by Anthony Hart, 4-Sep-2011)

Ref Expression
Assertion consym1 ψ ψ ψ φ

Proof

Step Hyp Ref Expression
1 falim ψ ψ ψ φ
2 1 ad2antll ψ ψ ψ ψ ψ φ
3 2 pm2.43i ψ ψ ψ φ