Theorem orim1d 962

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

Syntax hints:   → wi 4   ∨ wo 843

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 844

This theorem is referenced by:  pm2.38  965  pm2.8  969  pm2.73  970  pm2.74  971  pm2.82  972  moeq3  3689  unss1  4138  ordtri2or2  6268  gchor  10030  relin01  11145  icombl  24143  ioombl  24144  coltr  26414  frgrregorufrg  28084  cycpmco2  30777  fmlasuc  32635  satffunlem1lem2  32652  satffunlem2lem2  32655  naim1  33739  onsucconni  33787  dnibndlem13  33831  mblfinlem2  34959  leat3  36458  meetat2  36460  paddss1  36980