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  8058  soxp  8059  relin01  11638  nneo  12554  uzp1  12770  vdwlem9  16898  dfconn2  23332  fin1aufil  23845  dgrlt  26197  aalioulem2  26266  aalioulem5  26269  aalioulem6  26270  aaliou  26271  sqff1o  27117  disjpreima  32559  disjdsct  32679  voliune  34237  volfiniune  34238  satfvsucsuc  35397  naim2  36423  paddss2  39856  lzunuz  42800  acongneg2  43009  nneom  48558