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  3683  unss1  4148  ordtri2or2  6433  gchor  10580  relin01  11702  icombl  25465  ioombl  25466  coltr  28574  frgrregorufrg  30255  cycpmco2  33090  fmlasuc  35373  satffunlem1lem2  35390  satffunlem2lem2  35393  naim1  36377  onsucconni  36425  dnibndlem13  36478  mblfinlem2  37652  leat3  39288  meetat2  39290  paddss1  39811  onov0suclim  43263  dflim5  43318  ordsssucim  43391