Theorem orim2d 969

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 967	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ∨ wo 848

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 207  df-an 396  df-or 849

This theorem is referenced by:  orim2  970  pm2.82  978  axprglem  5378  poxp  8078  soxp  8079  relin01  11674  nneo  12613  uzp1  12825  vdwlem9  16960  dfconn2  23384  fin1aufil  23897  dgrlt  26231  aalioulem2  26299  aalioulem5  26302  aalioulem6  26303  aaliou  26304  sqff1o  27145  disjpreima  32654  disjdsct  32776  voliune  34373  volfiniune  34374  satfvsucsuc  35547  naim2  36572  paddss2  40264  lzunuz  43200  acongneg2  43405  nneom  49003