Metamath Proof Explorer

Theorem tsan1

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

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

Proof

Step Hyp Ref Expression
1 pm3.12 
 |-  ( ( -. ph \/ -. ps ) \/ ( ph /\ ps ) )
2 1 a1i 
 |-  ( th -> ( ( -. ph \/ -. ps ) \/ ( ph /\ ps ) ) )