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  8152  soxp  8153  relin01  11785  nneo  12700  uzp1  12917  vdwlem9  17023  dfconn2  23443  fin1aufil  23956  dgrlt  26321  aalioulem2  26390  aalioulem5  26393  aalioulem6  26394  aaliou  26395  sqff1o  27240  disjpreima  32604  disjdsct  32718  voliune  34210  volfiniune  34211  satfvsucsuc  35350  naim2  36373  paddss2  39801  lzunuz  42756  acongneg2  42966  nneom  48377