This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ex-or

Description: Example for df-or . Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion ex-or ( 2 = 3 ∨ 4 = 4 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ 4 = 4
2 1 olci ⊢ ( 2 = 3 ∨ 4 = 4 )