Metamath Proof Explorer

Theorem orsild

Description: A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 orsild.1 
 |-  ( ph -> -. ( ps \/ ch ) )
2 ioran 
 |-  ( -. ( ps \/ ch ) <-> ( -. ps /\ -. ch ) )
3 1 2 sylib 
 |-  ( ph -> ( -. ps /\ -. ch ) )
4 3 simpld 
 |-  ( ph -> -. ps )