Theorem orim1d 976

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

Syntax hints:   → wi 4   ∨ wo 856

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 209  df-an 399  df-or 857

This theorem is referenced by:  pm2.38  979  pm2.8  983  pm2.73  984  pm2.74  985  pm2.82  986  moeq3  3665  unss1  4128  axprglem  5383  ordtri2or2  6432  gchor  10571  relin01  11697  icombl  25595  ioombl  25596  coltr  28782  frgrregorufrg  30463  cycpmco2  33263  fmlasuc  35674  satffunlem1lem2  35691  satffunlem2lem2  35694  naim1  36687  onsucconni  36735  dnibndlem13  36866  mblfinlem2  38095  leat3  39857  meetat2  39859  paddss1  40379  onov0suclim  43789  dflim5  43844  ordsssucim  43917