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  3658  unss1  4125  axprglem  5378  ordtri2or2  6424  gchor  10550  relin01  11674  icombl  25531  ioombl  25532  coltr  28715  frgrregorufrg  30396  cycpmco2  33194  fmlasuc  35568  satffunlem1lem2  35585  satffunlem2lem2  35588  naim1  36571  onsucconni  36619  dnibndlem13  36750  mblfinlem2  37979  leat3  39741  meetat2  39743  paddss1  40263  onov0suclim  43702  dflim5  43757  ordsssucim  43830