Metamath Proof Explorer


Theorem orim1i

Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994)

Ref Expression
Hypothesis orim1i.1 ( 𝜑𝜓 )
Assertion orim1i ( ( 𝜑𝜒 ) → ( 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 orim1i.1 ( 𝜑𝜓 )
2 id ( 𝜒𝜒 )
3 1 2 orim12i ( ( 𝜑𝜒 ) → ( 𝜓𝜒 ) )