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  3670  unss1  4131  axprglem  5394  ordtri2or2  6457  gchor  10693  relin01  11821  icombl  25865  ioombl  25866  coltr  29098  frgrregorufrg  30909  cycpmco2  33676  fmlasuc  36120  satffunlem1lem2  36137  satffunlem2lem2  36140  naim1  37147  onsucconni  37195  dnibndlem13  37326  mblfinlem2  38544  dfprop2  38614  leat3  40320  meetat2  40322  paddss1  40842  onov0suclim  44234  dflim5  44289  ordsssucim  44362