Theorem orim1d 965

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-an 398  df-or 847

This theorem is referenced by:  pm2.38  968  pm2.8  972  pm2.73  973  pm2.74  974  pm2.82  975  moeq3  3709  unss1  4180  ordtri2or2  6464  gchor  10622  relin01  11738  icombl  25081  ioombl  25082  coltr  27929  frgrregorufrg  29610  cycpmco2  32323  fmlasuc  34408  satffunlem1lem2  34425  satffunlem2lem2  34428  naim1  35322  onsucconni  35370  dnibndlem13  35414  mblfinlem2  36574  leat3  38213  meetat2  38215  paddss1  38736  onov0suclim  42072  dflim5  42127  ordsssucim  42201