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 ( 𝜃 → ( ( ¬ 𝜑𝜓 ) ∨ ¬ ( 𝜑𝜓 ) ) )