Theorem orim1d 981

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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	orim12d 979	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  pm2.38  984  pm2.8  988  pm2.73  989  pm2.74  990  pm2.82  991  moeq3  3673  unss1  4134  axprglem  5405  ordtri2or2  6463  gchor  10640  relin01  11766  icombl  25798  ioombl  25799  coltr  29003  frgrregorufrg  30814  cycpmco2  33581  fmlasuc  35973  satffunlem1lem2  35990  satffunlem2lem2  35993  naim1  37016  onsucconni  37064  dnibndlem13  37195  mblfinlem2  38415  leat3  40176  meetat2  40178  paddss1  40698  onov0suclim  44123  dflim5  44178  ordsssucim  44251