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  5409  poxp  8125  soxp  8126  relin01  11739  nneo  12681  uzp1  12900  vdwlem9  17050  dfconn2  23557  fin1aufil  24070  dgrlt  26404  aalioulem2  26475  aalioulem5  26478  aalioulem6  26479  aaliou  26480  sqff1o  27324  disjpreima  32907  disjdsct  33026  voliune  34597  volfiniune  34598  satfvsucsuc  35835  naim2  36879  paddss2  40570  lzunuz  43479  acongneg2  43684  nneom  49284