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  31846  disjdsct  31955  voliune  33258  volfiniune  33259  satfvsucsuc  34387  naim2  35323  paddss2  38737  lzunuz  41554  acongneg2  41764  nneom  47261