Theorem orim1d 966

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 965	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 207  df-an 396  df-or 847

This theorem is referenced by:  pm2.38  969  pm2.8  973  pm2.73  974  pm2.74  975  pm2.82  976  moeq3  3734  unss1  4208  ordtri2or2  6494  gchor  10696  relin01  11814  icombl  25618  ioombl  25619  coltr  28673  frgrregorufrg  30358  cycpmco2  33126  fmlasuc  35354  satffunlem1lem2  35371  satffunlem2lem2  35374  naim1  36355  onsucconni  36403  dnibndlem13  36456  mblfinlem2  37618  leat3  39251  meetat2  39253  paddss1  39774  onov0suclim  43236  dflim5  43291  ordsssucim  43364