Metamath Proof Explorer


Theorem ts3an2

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

Ref Expression
Assertion ts3an2
|- ( th -> ( ( ph /\ ps ) \/ -. ( ph /\ ps /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 tsan2
 |-  ( th -> ( ( ph /\ ps ) \/ -. ( ( ph /\ ps ) /\ ch ) ) )
2 df-3an
 |-  ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
3 2 notbii
 |-  ( -. ( ph /\ ps /\ ch ) <-> -. ( ( ph /\ ps ) /\ ch ) )
4 3 orbi2i
 |-  ( ( ( ph /\ ps ) \/ -. ( ph /\ ps /\ ch ) ) <-> ( ( ph /\ ps ) \/ -. ( ( ph /\ ps ) /\ ch ) ) )
5 1 4 sylibr
 |-  ( th -> ( ( ph /\ ps ) \/ -. ( ph /\ ps /\ ch ) ) )