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  3673  unss1  4186  axprglem  5398  ordtri2or2  6482  gchor  10739  relin01  11867  icombl  25915  ioombl  25916  coltr  29146  frgrregorufrg  30957  cycpmco2  33764  fmlasuc  36318  satffunlem1lem2  36335  satffunlem2lem2  36338  naim1  37355  onsucconni  37403  dnibndlem13  37534  mblfinlem2  38768  dfprop2  38838  leat3  40544  meetat2  40546  paddss1  41066  onov0suclim  44468  dflim5  44523  ordsssucim  44596