Metamath Proof Explorer

Theorem orim1d

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995)

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

Proof

Step Hyp Ref Expression
1 orim1d.1 
 |-  ( ph -> ( ps -> ch ) )
2 idd 
 |-  ( ph -> ( th -> th ) )
3 1 2 orim12d 
 |-  ( ph -> ( ( ps \/ th ) -> ( ch \/ th ) ) )