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  3686  unss1  4151  ordtri2or2  6436  gchor  10587  relin01  11709  icombl  25472  ioombl  25473  coltr  28581  frgrregorufrg  30262  cycpmco2  33097  fmlasuc  35380  satffunlem1lem2  35397  satffunlem2lem2  35400  naim1  36384  onsucconni  36432  dnibndlem13  36485  mblfinlem2  37659  leat3  39295  meetat2  39297  paddss1  39818  onov0suclim  43270  dflim5  43325  ordsssucim  43398