Theorem orim2d 982

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		orim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	orim12d 979	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  orim2  983  pm2.82  991  axprglem  5399  poxp  8170  soxp  8171  relin01  11870  nneo  12813  uzp1  13032  vdwlem9  17199  dfconn2  23770  fin1aufil  24284  dgrlt  26618  aalioulem2  26693  aalioulem5  26696  aalioulem6  26697  aaliou  26698  sqff1o  27542  disjpreima  33253  disjdsct  33370  voliune  34945  volfiniune  34946  satfvsucsuc  36310  naim2  37369  dfprop2  38851  paddss2  41078  lzunuz  43983  acongneg2  44188  nneom  49854