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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  orim2  983  pm2.82  991  axprglem  5412  poxp  8133  soxp  8134  relin01  11756  nneo  12698  uzp1  12917  vdwlem9  17074  dfconn2  23613  fin1aufil  24126  dgrlt  26460  aalioulem2  26533  aalioulem5  26536  aalioulem6  26537  aaliou  26538  sqff1o  27383  disjpreima  32966  disjdsct  33085  voliune  34651  volfiniune  34652  satfvsucsuc  35878  naim2  36942  paddss2  40633  lzunuz  43540  acongneg2  43745  nneom  49348