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 209  df-an 399  df-or 844

This theorem is referenced by:  orim2  964  pm2.82  972  poxp  7814  soxp  7815  relin01  11156  nneo  12058  uzp1  12271  vdwlem9  16317  dfconn2  22019  fin1aufil  22532  dgrlt  24848  aalioulem2  24914  aalioulem5  24917  aalioulem6  24918  aaliou  24919  sqff1o  25751  disjpreima  30326  disjdsct  30430  voliune  31481  volfiniune  31482  satfvsucsuc  32605  naim2  33731  paddss2  36946  lzunuz  39355  acongneg2  39564  nneom  44577