Theorem orim1d 964

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

Syntax hints:   → wi 4   ∨ wo 845

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 210  df-an 401  df-or 846

This theorem is referenced by:  pm2.38  967  pm2.8  971  pm2.73  972  pm2.74  973  pm2.82  974  moeq3  3627  unss1  4085  ordtri2or2  6263  gchor  10077  relin01  11192  icombl  24254  ioombl  24255  coltr  26530  frgrregorufrg  28200  cycpmco2  30916  fmlasuc  32854  satffunlem1lem2  32871  satffunlem2lem2  32874  naim1  34117  onsucconni  34165  dnibndlem13  34209  mblfinlem2  35365  leat3  36861  meetat2  36863  paddss1  37383