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  5382  poxp  8080  soxp  8081  relin01  11673  nneo  12588  uzp1  12800  vdwlem9  16929  dfconn2  23375  fin1aufil  23888  dgrlt  26240  aalioulem2  26309  aalioulem5  26312  aalioulem6  26313  aaliou  26314  sqff1o  27160  disjpreima  32670  disjdsct  32792  voliune  34406  volfiniune  34407  satfvsucsuc  35578  naim2  36603  paddss2  40188  lzunuz  43119  acongneg2  43328  nneom  48881