Theorem orim1d 963

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

Syntax hints:   → wi 4   ∨ wo 844

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 206  df-an 397  df-or 845

This theorem is referenced by:  pm2.38  966  pm2.8  970  pm2.73  971  pm2.74  972  pm2.82  973  moeq3  3657  unss1  4125  ordtri2or2  6394  gchor  10476  relin01  11592  icombl  24826  ioombl  24827  coltr  27238  frgrregorufrg  28919  cycpmco2  31628  fmlasuc  33588  satffunlem1lem2  33605  satffunlem2lem2  33608  naim1  34669  onsucconni  34717  dnibndlem13  34761  mblfinlem2  35913  leat3  37555  meetat2  37557  paddss1  38078  dflim5  41303