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  8068  soxp  8069  relin01  11662  nneo  12578  uzp1  12794  vdwlem9  16919  dfconn2  23322  fin1aufil  23835  dgrlt  26188  aalioulem2  26257  aalioulem5  26260  aalioulem6  26261  aaliou  26262  sqff1o  27108  disjpreima  32546  disjdsct  32659  voliune  34195  volfiniune  34196  satfvsucsuc  35337  naim2  36363  paddss2  39797  lzunuz  42741  acongneg2  42950  nneom  48513