Theorem orim1d 978

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  pm2.38  981  pm2.8  985  pm2.73  986  pm2.74  987  pm2.82  988  moeq3  3674  unss1  4137  axprglem  5392  ordtri2or2  6443  gchor  10582  relin01  11708  icombl  25606  ioombl  25607  coltr  28793  frgrregorufrg  30474  cycpmco2  33274  fmlasuc  35700  satffunlem1lem2  35717  satffunlem2lem2  35720  naim1  36713  onsucconni  36761  dnibndlem13  36892  mblfinlem2  38121  leat3  39883  meetat2  39885  paddss1  40405  onov0suclim  43815  dflim5  43870  ordsssucim  43943