Metamath Proof Explorer

Theorem orrd

Description: Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995)

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

Proof

Step Hyp Ref Expression
1 orrd.1 
 |-  ( ph -> ( -. ps -> ch ) )
2 pm2.54 
 |-  ( ( -. ps -> ch ) -> ( ps \/ ch ) )
3 1 2 syl 
 |-  ( ph -> ( ps \/ ch ) )