Metamath Proof Explorer

Theorem orim2d

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

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

Proof

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