Theorem orim2d 963

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

Syntax hints:   → wi 4   ∨ wo 843

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 209  df-an 399  df-or 844

This theorem is referenced by:  orim2  964  pm2.82  972  poxp  7822  soxp  7823  relin01  11164  nneo  12067  uzp1  12280  vdwlem9  16325  dfconn2  22027  fin1aufil  22540  dgrlt  24856  aalioulem2  24922  aalioulem5  24925  aalioulem6  24926  aaliou  24927  sqff1o  25759  disjpreima  30334  disjdsct  30438  voliune  31488  volfiniune  31489  satfvsucsuc  32612  naim2  33738  paddss2  36969  lzunuz  39385  acongneg2  39594  nneom  44607