Theorem orim1d 963

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

Syntax hints:   → wi 4   ∨ wo 844

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 400  df-or 845

This theorem is referenced by:  pm2.38  966  pm2.8  970  pm2.73  971  pm2.74  972  pm2.82  973  moeq3  3651  unss1  4106  ordtri2or2  6255  gchor  10038  relin01  11153  icombl  24168  ioombl  24169  coltr  26441  frgrregorufrg  28111  cycpmco2  30825  fmlasuc  32746  satffunlem1lem2  32763  satffunlem2lem2  32766  naim1  33850  onsucconni  33898  dnibndlem13  33942  mblfinlem2  35095  leat3  36591  meetat2  36593  paddss1  37113