Theorem orim1d 884

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

Syntax hints:   → wi 4   ∨ wo 383

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 197  df-or 385  df-an 386

This theorem is referenced by:  pm2.38  887  pm2.73  890  pm2.74  891  pm2.8  895  pm2.82  897  moeq3  3383  unss1  3782  ordtri2or2  5823  gchor  9449  relin01  10552  icombl  23332  ioombl  23333  coltr  25542  frgrregorufrg  27190  naim1  32384  onsucconni  32436  dnibndlem13  32480  mblfinlem2  33447  leat3  34582  meetat2  34584  paddss1  35103