Theorem orim2d 974

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

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  orim2  975  pm2.82  983  axprglem  5372  poxp  8075  soxp  8076  relin01  11672  nneo  12611  uzp1  12823  vdwlem9  16958  dfconn2  23409  fin1aufil  23922  dgrlt  26256  aalioulem2  26324  aalioulem5  26327  aalioulem6  26328  aaliou  26329  sqff1o  27170  disjpreima  32680  disjdsct  32802  voliune  34420  volfiniune  34421  satfvsucsuc  35600  naim2  36625  paddss2  40317  lzunuz  43224  acongneg2  43429  nneom  49025