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 ( ( 𝜓 ∨ ( 𝜓 ∨ ⊥ ) ) → ( 𝜓𝜑 ) )