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 ) ) )