Metamath Proof Explorer

Theorem notornotel2

Description: A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018)

Ref Expression
Hypothesis notornotel2.1 
|- ( ph -> -. ( ps \/ -. ch ) )
Assertion notornotel2 
|- ( ph -> ch )

Proof

Step Hyp Ref Expression
1 notornotel2.1 
 |-  ( ph -> -. ( ps \/ -. ch ) )
2 orcom 
 |-  ( ( -. ch \/ ps ) <-> ( ps \/ -. ch ) )
3 1 2 sylnibr 
 |-  ( ph -> -. ( -. ch \/ ps ) )
4 3 notornotel1 
 |-  ( ph -> ch )