Metamath Proof Explorer


Theorem tsor1

Description: A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018)

Ref Expression
Assertion tsor1 θ φ ψ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 exmidd θ φ ψ ¬ φ ψ