Metamath Proof Explorer

Theorem orsird

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

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

Proof

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