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  8064  soxp  8065  relin01  11648  nneo  12563  uzp1  12775  vdwlem9  16903  dfconn2  23335  fin1aufil  23848  dgrlt  26200  aalioulem2  26269  aalioulem5  26272  aalioulem6  26273  aaliou  26274  sqff1o  27120  disjpreima  32566  disjdsct  32688  voliune  34263  volfiniune  34264  satfvsucsuc  35430  naim2  36455  paddss2  39937  lzunuz  42885  acongneg2  43094  nneom  48652