Theorem orim2d 968

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 966	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  orim2  969  pm2.82  977  poxp  8070  soxp  8071  relin01  11661  nneo  12576  uzp1  12788  vdwlem9  16917  dfconn2  23363  fin1aufil  23876  dgrlt  26228  aalioulem2  26297  aalioulem5  26300  aalioulem6  26301  aaliou  26302  sqff1o  27148  disjpreima  32659  disjdsct  32782  voliune  34386  volfiniune  34387  satfvsucsuc  35559  naim2  36584  paddss2  40074  lzunuz  43006  acongneg2  43215  nneom  48769