Metamath Proof Explorer

Theorem tsim1

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

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

Proof

Step Hyp Ref Expression
1 exmid 
 |-  ( ( ph -> ps ) \/ -. ( ph -> ps ) )
2 df-or 
 |-  ( ( -. ph \/ ps ) <-> ( -. -. ph -> ps ) )
3 notnotb 
 |-  ( ph <-> -. -. ph )
4 3 bicomi 
 |-  ( -. -. ph <-> ph )
5 4 imbi1i 
 |-  ( ( -. -. ph -> ps ) <-> ( ph -> ps ) )
6 2 5 bitri 
 |-  ( ( -. ph \/ ps ) <-> ( ph -> ps ) )
7 6 orbi1i 
 |-  ( ( ( -. ph \/ ps ) \/ -. ( ph -> ps ) ) <-> ( ( ph -> ps ) \/ -. ( ph -> ps ) ) )
8 1 7 mpbir 
 |-  ( ( -. ph \/ ps ) \/ -. ( ph -> ps ) )
9 8 a1i 
 |-  ( th -> ( ( -. ph \/ ps ) \/ -. ( ph -> ps ) ) )