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  5394  poxp  8129  soxp  8130  relin01  11821  nneo  12764  uzp1  12983  vdwlem9  17147  dfconn2  23717  fin1aufil  24231  dgrlt  26565  aalioulem2  26642  aalioulem5  26645  aalioulem6  26646  aaliou  26647  sqff1o  27491  disjpreima  33160  disjdsct  33278  voliune  34844  volfiniune  34845  satfvsucsuc  36099  naim2  37148  dfprop2  38614  paddss2  40843  lzunuz  43732  acongneg2  43937  nneom  49583