Metamath Proof Explorer

Theorem orel2

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.56 of WhiteheadRussell p. 107. (Contributed by NM, 12-Aug-1994) (Proof shortened by Wolf Lammen, 5-Apr-2013)

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

Proof

Step Hyp Ref Expression
1 idd 
 |-  ( -. ph -> ( ps -> ps ) )
2 pm2.21 
 |-  ( -. ph -> ( ph -> ps ) )
3 1 2 jaod 
 |-  ( -. ph -> ( ( ps \/ ph ) -> ps ) )