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  5373  poxp  8071  soxp  8072  relin01  11665  nneo  12604  uzp1  12816  vdwlem9  16951  dfconn2  23394  fin1aufil  23907  dgrlt  26241  aalioulem2  26310  aalioulem5  26313  aalioulem6  26314  aaliou  26315  sqff1o  27159  disjpreima  32669  disjdsct  32791  voliune  34389  volfiniune  34390  satfvsucsuc  35563  naim2  36588  paddss2  40278  lzunuz  43214  acongneg2  43423  nneom  49015