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