Theorem orim2d 967

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 965	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 210  df-an 400  df-or 848

This theorem is referenced by:  orim2  968  pm2.82  976  poxp  7895  soxp  7896  relin01  11356  nneo  12261  uzp1  12475  vdwlem9  16542  dfconn2  22316  fin1aufil  22829  dgrlt  25160  aalioulem2  25226  aalioulem5  25229  aalioulem6  25230  aaliou  25231  sqff1o  26064  disjpreima  30642  disjdsct  30755  voliune  31909  volfiniune  31910  satfvsucsuc  33040  naim2  34316  paddss2  37569  lzunuz  40293  acongneg2  40502  nneom  45546