Theorem orim1d 973

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 972	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃)))

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  pm2.38  976  pm2.8  980  pm2.73  981  pm2.74  982  pm2.82  983  moeq3  3660  unss1  4121  axprglem  5372  ordtri2or2  6418  gchor  10548  relin01  11672  icombl  25556  ioombl  25557  coltr  28740  frgrregorufrg  30421  cycpmco2  33221  fmlasuc  35621  satffunlem1lem2  35638  satffunlem2lem2  35641  naim1  36624  onsucconni  36672  dnibndlem13  36803  mblfinlem2  38032  leat3  39794  meetat2  39796  paddss1  40316  onov0suclim  43726  dflim5  43781  ordsssucim  43854