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  8127  soxp  8128  relin01  11761  nneo  12677  uzp1  12893  vdwlem9  17009  dfconn2  23357  fin1aufil  23870  dgrlt  26224  aalioulem2  26293  aalioulem5  26296  aalioulem6  26297  aaliou  26298  sqff1o  27144  disjpreima  32565  disjdsct  32680  voliune  34260  volfiniune  34261  satfvsucsuc  35387  naim2  36408  paddss2  39837  lzunuz  42791  acongneg2  43001  nneom  48507