Theorem orim1d 993

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

Syntax hints:   → wi 4   ∨ wo 878

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 199  df-an 387  df-or 879

This theorem is referenced by:  pm2.38  996  pm2.8  1000  pm2.73  1001  pm2.74  1002  pm2.82  1003  moeq3  3608  unss1  4011  ordtri2or2  6063  gchor  9771  relin01  10883  icombl  23737  ioombl  23738  coltr  25966  frgrregorufrg  27703  naim1  32917  onsucconni  32964  dnibndlem13  33008  mblfinlem2  33990  leat3  35369  meetat2  35371  paddss1  35891