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  poxp  8153  soxp  8154  relin01  11787  nneo  12702  uzp1  12919  vdwlem9  17027  dfconn2  23427  fin1aufil  23940  dgrlt  26306  aalioulem2  26375  aalioulem5  26378  aalioulem6  26379  aaliou  26380  sqff1o  27225  disjpreima  32597  disjdsct  32712  voliune  34230  volfiniune  34231  satfvsucsuc  35370  naim2  36391  paddss2  39820  lzunuz  42779  acongneg2  42989  nneom  48448