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  3671  unss1  4135  ordtri2or2  6407  gchor  10515  relin01  11638  icombl  25490  ioombl  25491  coltr  28623  frgrregorufrg  30301  cycpmco2  33097  fmlasuc  35418  satffunlem1lem2  35435  satffunlem2lem2  35438  naim1  36422  onsucconni  36470  dnibndlem13  36523  mblfinlem2  37697  leat3  39333  meetat2  39335  paddss1  39855  onov0suclim  43306  dflim5  43361  ordsssucim  43434