Theorem orim1d 880

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

Syntax hints:   → wi 4   ∨ wo 382

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 196  df-or 384  df-an 385

This theorem is referenced by:  pm2.38  883  pm2.73  886  pm2.74  887  pm2.8  891  pm2.82  893  moeq3  3350  unss1  3744  ordtri2or2  5740  gchor  9328  relin01  10431  icombl  23139  ioombl  23140  coltr  25342  frgraregorufrg  26599  naim1  31554  onsucconi  31606  dnibndlem13  31650  mblfinlem2  32617  leat3  33600  meetat2  33602  paddss1  34121  frgrregorufrg  41505