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
|- ( th -> ( ( -. ph \/ ps ) \/ -. ( ph <-> ps ) ) )

Proof

Step Hyp Ref Expression
1 tsbi3
 |-  ( th -> ( ( ps \/ -. ph ) \/ -. ( ps <-> ph ) ) )
2 orcom
 |-  ( ( ps \/ -. ph ) <-> ( -. ph \/ ps ) )
3 bicom
 |-  ( ( ps <-> ph ) <-> ( ph <-> ps ) )
4 3 notbii
 |-  ( -. ( ps <-> ph ) <-> -. ( ph <-> ps ) )
5 2 4 orbi12i
 |-  ( ( ( ps \/ -. ph ) \/ -. ( ps <-> ph ) ) <-> ( ( -. ph \/ ps ) \/ -. ( ph <-> ps ) ) )
6 1 5 sylib
 |-  ( th -> ( ( -. ph \/ ps ) \/ -. ( ph <-> ps ) ) )