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
|- ( ( ps \/ ( ps \/ F. ) ) -> ( ps \/ ph ) )

Proof

Step Hyp Ref Expression
1 orc
 |-  ( ps -> ( ps \/ ph ) )
2 falim
 |-  ( F. -> ph )
3 2 orim2i
 |-  ( ( ps \/ F. ) -> ( ps \/ ph ) )
4 1 3 jaoi
 |-  ( ( ps \/ ( ps \/ F. ) ) -> ( ps \/ ph ) )