Metamath Proof Explorer


Theorem tsbi3

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

Ref Expression
Assertion tsbi3 θ φ ¬ ψ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 biimpr φ ψ ψ φ
2 con34b ψ φ ¬ φ ¬ ψ
3 pm2.54 ¬ φ ¬ ψ φ ¬ ψ
4 2 3 sylbi ψ φ φ ¬ ψ
5 1 4 syl φ ψ φ ¬ ψ
6 5 con3i ¬ φ ¬ ψ ¬ φ ψ
7 6 orri φ ¬ ψ ¬ φ ψ
8 7 a1i θ φ ¬ ψ ¬ φ ψ