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  5393  poxp  8142  soxp  8143  relin01  11843  nneo  12786  uzp1  13005  vdwlem9  17172  dfconn2  23742  fin1aufil  24256  dgrlt  26590  aalioulem2  26665  aalioulem5  26668  aalioulem6  26669  aaliou  26670  sqff1o  27514  disjpreima  33225  disjdsct  33343  voliune  34908  volfiniune  34909  satfvsucsuc  36216  naim2  37270  dfprop2  38739  paddss2  40968  lzunuz  43872  acongneg2  44077  nneom  49732