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  3667  unss1  4134  ordtri2or2  6412  gchor  10525  relin01  11648  icombl  25493  ioombl  25494  coltr  28626  frgrregorufrg  30308  cycpmco2  33109  fmlasuc  35451  satffunlem1lem2  35468  satffunlem2lem2  35471  naim1  36454  onsucconni  36502  dnibndlem13  36555  mblfinlem2  37718  leat3  39414  meetat2  39416  paddss1  39936  onov0suclim  43391  dflim5  43446  ordsssucim  43519