Theorem orim1d 981

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)

Hypothesis

Ref	Expression
orim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
orim1d	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃)))

Proof of Theorem orim1d

Step	Hyp	Ref	Expression
1		orim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 25	. 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:  pm2.38  984  pm2.8  988  pm2.73  989  pm2.74  990  pm2.82  991  moeq3  3669  unss1  4183  axprglem  5393  ordtri2or2  6464  gchor  10715  relin01  11843  icombl  25890  ioombl  25891  coltr  29121  frgrregorufrg  30932  cycpmco2  33740  fmlasuc  36237  satffunlem1lem2  36254  satffunlem2lem2  36257  naim1  37269  onsucconni  37317  dnibndlem13  37448  mblfinlem2  38669  dfprop2  38739  leat3  40445  meetat2  40447  paddss1  40967  onov0suclim  44369  dflim5  44424  ordsssucim  44497