Theorem orim1d 967

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  pm2.38  970  pm2.8  974  pm2.73  975  pm2.74  976  pm2.82  977  moeq3  3672  unss1  4136  ordtri2or2  6408  gchor  10521  relin01  11644  icombl  25463  ioombl  25464  coltr  28592  frgrregorufrg  30270  cycpmco2  33075  fmlasuc  35359  satffunlem1lem2  35376  satffunlem2lem2  35379  naim1  36363  onsucconni  36411  dnibndlem13  36464  mblfinlem2  37638  leat3  39274  meetat2  39276  paddss1  39796  onov0suclim  43247  dflim5  43302  ordsssucim  43375