Theorem orim2d 982

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		orim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	orim12d 979	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  orim2  983  pm2.82  991  axprglem  5405  poxp  8130  soxp  8131  relin01  11766  nneo  12709  uzp1  12928  vdwlem9  17087  dfconn2  23650  fin1aufil  24164  dgrlt  26499  aalioulem2  26576  aalioulem5  26579  aalioulem6  26580  aaliou  26581  sqff1o  27426  disjpreima  33065  disjdsct  33183  voliune  34748  volfiniune  34749  satfvsucsuc  35952  naim2  37017  paddss2  40699  lzunuz  43621  acongneg2  43826  nneom  49465