Theorem orim1d 968

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  pm2.38  971  pm2.8  975  pm2.73  976  pm2.74  977  pm2.82  978  moeq3  3659  unss1  4126  axprglem  5373  ordtri2or2  6418  gchor  10541  relin01  11665  icombl  25541  ioombl  25542  coltr  28729  frgrregorufrg  30411  cycpmco2  33209  fmlasuc  35584  satffunlem1lem2  35601  satffunlem2lem2  35604  naim1  36587  onsucconni  36635  dnibndlem13  36766  mblfinlem2  37993  leat3  39755  meetat2  39757  paddss1  40277  onov0suclim  43720  dflim5  43775  ordsssucim  43848