Theorem orim2d 982

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		orim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	orim12d 979	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  orim2  983  pm2.82  991  axprglem  5398  poxp  8112  soxp  8113  relin01  11726  nneo  12671  uzp1  12890  vdwlem9  17039  dfconn2  23537  fin1aufil  24050  dgrlt  26384  aalioulem2  26455  aalioulem5  26458  aalioulem6  26459  aaliou  26460  sqff1o  27304  disjpreima  32839  disjdsct  32960  voliune  34536  volfiniune  34537  satfvsucsuc  35728  naim2  36763  paddss2  40454  lzunuz  43361  acongneg2  43566  nneom  49158