Theorem orim1d 968

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  pm2.38  971  pm2.8  975  pm2.73  976  pm2.74  977  pm2.82  978  moeq3  3672  unss1  4139  axprglem  5382  ordtri2or2  6426  gchor  10550  relin01  11673  icombl  25533  ioombl  25534  coltr  28731  frgrregorufrg  30413  cycpmco2  33226  fmlasuc  35599  satffunlem1lem2  35616  satffunlem2lem2  35619  naim1  36602  onsucconni  36650  dnibndlem13  36709  mblfinlem2  37903  leat3  39665  meetat2  39667  paddss1  40187  onov0suclim  43625  dflim5  43680  ordsssucim  43753