Metamath Proof Explorer

Theorem tsim2

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

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

Proof

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