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 206  df-an 397  df-or 845

This theorem is referenced by:  pm2.38  966  pm2.8  970  pm2.73  971  pm2.74  972  pm2.82  973  moeq3  3647  unss1  4113  ordtri2or2  6362  gchor  10383  relin01  11499  icombl  24728  ioombl  24729  coltr  27008  frgrregorufrg  28690  cycpmco2  31400  fmlasuc  33348  satffunlem1lem2  33365  satffunlem2lem2  33368  naim1  34578  onsucconni  34626  dnibndlem13  34670  mblfinlem2  35815  leat3  37309  meetat2  37311  paddss1  37831