Metamath Proof Explorer


Theorem tsim3

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

Ref Expression
Assertion tsim3 θ¬ψφψ

Proof

Step Hyp Ref Expression
1 ax-1 ψφψ
2 1 imori ¬ψφψ
3 2 a1i θ¬ψφψ