Metamath Proof Explorer


Theorem tsbi1

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

Ref Expression
Assertion tsbi1 ( 𝜃 → ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ∨ ( 𝜑𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 pm5.1 ( ( 𝜑𝜓 ) → ( 𝜑𝜓 ) )
2 1 olcd ( ( 𝜑𝜓 ) → ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ∨ ( 𝜑𝜓 ) ) )
3 pm3.13 ( ¬ ( 𝜑𝜓 ) → ( ¬ 𝜑 ∨ ¬ 𝜓 ) )
4 3 orcd ( ¬ ( 𝜑𝜓 ) → ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ∨ ( 𝜑𝜓 ) ) )
5 2 4 pm2.61i ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ∨ ( 𝜑𝜓 ) )
6 5 a1i ( 𝜃 → ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ∨ ( 𝜑𝜓 ) ) )