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  3678  unss1  4141  axprglem  5412  ordtri2or2  6469  gchor  10630  relin01  11756  icombl  25760  ioombl  25761  coltr  28958  frgrregorufrg  30714  cycpmco2  33484  fmlasuc  35899  satffunlem1lem2  35916  satffunlem2lem2  35919  naim1  36941  onsucconni  36989  dnibndlem13  37120  mblfinlem2  38350  leat3  40110  meetat2  40112  paddss1  40632  onov0suclim  44042  dflim5  44097  ordsssucim  44170