Metamath Proof Explorer


Theorem tsbi4

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

Ref Expression
Assertion tsbi4 θ ¬ φ ψ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 tsbi3 θ ψ ¬ φ ¬ ψ φ
2 orcom ψ ¬ φ ¬ φ ψ
3 bicom ψ φ φ ψ
4 3 notbii ¬ ψ φ ¬ φ ψ
5 2 4 orbi12i ψ ¬ φ ¬ ψ φ ¬ φ ψ ¬ φ ψ
6 1 5 sylib θ ¬ φ ψ ¬ φ ψ