Theorem orim2d 968

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  orim2  969  pm2.82  977  poxp  8107  soxp  8108  relin01  11702  nneo  12618  uzp1  12834  vdwlem9  16960  dfconn2  23306  fin1aufil  23819  dgrlt  26172  aalioulem2  26241  aalioulem5  26244  aalioulem6  26245  aaliou  26246  sqff1o  27092  disjpreima  32513  disjdsct  32626  voliune  34219  volfiniune  34220  satfvsucsuc  35352  naim2  36378  paddss2  39812  lzunuz  42756  acongneg2  42966  nneom  48516