Theorem orim2d 990

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

Syntax hints:   → wi 4   ∨ wo 874

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 199  df-an 386  df-or 875

This theorem is referenced by:  orim2  991  pm2.82  999  poxp  7524  soxp  7525  relin01  10842  nneo  11747  uzp1  11961  vdwlem9  16023  dfconn2  21548  fin1aufil  22061  dgrlt  24360  aalioulem2  24426  aalioulem5  24429  aalioulem6  24430  aaliou  24431  sqff1o  25257  disjpreima  29906  disjdsct  29990  voliune  30800  volfiniune  30801  naim2  32889  paddss2  35831  lzunuz  38105  acongneg2  38317  nneom  43108