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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  pm2.38  984  pm2.8  988  pm2.73  989  pm2.74  990  pm2.82  991  moeq3  3678  unss1  4140  axprglem  5398  ordtri2or2  6451  gchor  10600  relin01  11726  icombl  25684  ioombl  25685  coltr  28875  frgrregorufrg  30586  cycpmco2  33366  fmlasuc  35749  satffunlem1lem2  35766  satffunlem2lem2  35769  naim1  36762  onsucconni  36810  dnibndlem13  36941  mblfinlem2  38169  leat3  39931  meetat2  39933  paddss1  40453  onov0suclim  43863  dflim5  43918  ordsssucim  43991