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 206  df-an 396  df-or 844

This theorem is referenced by:  pm2.38  965  pm2.8  969  pm2.73  970  pm2.74  971  pm2.82  972  moeq3  3642  unss1  4109  ordtri2or2  6347  gchor  10314  relin01  11429  icombl  24633  ioombl  24634  coltr  26912  frgrregorufrg  28591  cycpmco2  31302  fmlasuc  33248  satffunlem1lem2  33265  satffunlem2lem2  33268  naim1  34505  onsucconni  34553  dnibndlem13  34597  mblfinlem2  35742  leat3  37236  meetat2  37238  paddss1  37758