Metamath Proof Explorer

Theorem orcanai

Description: Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994)

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

Proof

Step Hyp Ref Expression
1 orcanai.1 
 |-  ( ph -> ( ps \/ ch ) )
2 1 ord 
 |-  ( ph -> ( -. ps -> ch ) )
3 2 imp 
 |-  ( ( ph /\ -. ps ) -> ch )