Metamath Proof Explorer


Theorem dissym1

Description: A symmetry with \/ .

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

Ref Expression
Assertion dissym1 ψψψφ

Proof

Step Hyp Ref Expression
1 orc ψψφ
2 falim φ
3 2 orim2i ψψφ
4 1 3 jaoi ψψψφ