Theorem orim2d 964

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

Hypothesis

Ref	Expression
orim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
orim2d	⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

Proof of Theorem orim2d

Step	Hyp	Ref	Expression
1		idd 24	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		orim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	orim12d 962	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ∨ wo 844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845

This theorem is referenced by:  orim2  965  pm2.82  973  poxp  7805  soxp  7806  relin01  11153  nneo  12054  uzp1  12267  vdwlem9  16315  dfconn2  22024  fin1aufil  22537  dgrlt  24863  aalioulem2  24929  aalioulem5  24932  aalioulem6  24933  aaliou  24934  sqff1o  25767  disjpreima  30347  disjdsct  30462  voliune  31598  volfiniune  31599  satfvsucsuc  32725  naim2  33851  paddss2  37114  lzunuz  39709  acongneg2  39918  nneom  44941