Theorem orim2d 969

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  orim2  970  pm2.82  978  axprglem  5379  poxp  8080  soxp  8081  relin01  11676  nneo  12615  uzp1  12827  vdwlem9  16962  dfconn2  23386  fin1aufil  23899  dgrlt  26233  aalioulem2  26301  aalioulem5  26304  aalioulem6  26305  aaliou  26306  sqff1o  27147  disjpreima  32656  disjdsct  32778  voliune  34375  volfiniune  34376  satfvsucsuc  35549  naim2  36574  paddss2  40266  lzunuz  43202  acongneg2  43407  nneom  49005