Theorem orim2d 979

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  orim2  980  pm2.82  988  axprglem  5392  poxp  8103  soxp  8104  relin01  11708  nneo  12654  uzp1  12873  vdwlem9  17008  dfconn2  23459  fin1aufil  23972  dgrlt  26306  aalioulem2  26374  aalioulem5  26377  aalioulem6  26378  aaliou  26379  sqff1o  27223  disjpreima  32733  disjdsct  32855  voliune  34487  volfiniune  34488  satfvsucsuc  35679  naim2  36714  paddss2  40406  lzunuz  43313  acongneg2  43518  nneom  49113