Theorem orim1d 981

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	orim12d 979	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃)))

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  pm2.38  984  pm2.8  988  pm2.73  989  pm2.74  990  pm2.82  991  moeq3  3676  unss1  4139  axprglem  5409  ordtri2or2  6464  gchor  10613  relin01  11739  icombl  25704  ioombl  25705  coltr  28899  frgrregorufrg  30655  cycpmco2  33431  fmlasuc  35856  satffunlem1lem2  35873  satffunlem2lem2  35876  naim1  36878  onsucconni  36926  dnibndlem13  37057  mblfinlem2  38287  leat3  40047  meetat2  40049  paddss1  40569  onov0suclim  43981  dflim5  44036  ordsssucim  44109