Theorem orim2d 963

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

Syntax hints:   → wi 4   ∨ wo 843

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 206  df-an 396  df-or 844

This theorem is referenced by:  orim2  964  pm2.82  972  poxp  7953  soxp  7954  relin01  11482  nneo  12387  uzp1  12601  vdwlem9  16671  dfconn2  22551  fin1aufil  23064  dgrlt  25408  aalioulem2  25474  aalioulem5  25477  aalioulem6  25478  aaliou  25479  sqff1o  26312  disjpreima  30902  disjdsct  31014  voliune  32176  volfiniune  32177  satfvsucsuc  33306  naim2  34558  paddss2  37811  lzunuz  40570  acongneg2  40779  nneom  45825