Theorem orim2d 966

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-an 398  df-or 847

This theorem is referenced by:  orim2  967  pm2.82  975  poxp  8114  soxp  8115  relin01  11738  nneo  12646  uzp1  12863  vdwlem9  16922  dfconn2  22923  fin1aufil  23436  dgrlt  25780  aalioulem2  25846  aalioulem5  25849  aalioulem6  25850  aaliou  25851  sqff1o  26686  disjpreima  31815  disjdsct  31924  voliune  33227  volfiniune  33228  satfvsucsuc  34356  naim2  35275  paddss2  38689  lzunuz  41506  acongneg2  41716  nneom  47213