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

This theorem is referenced by:  pm2.38  967  pm2.8  971  pm2.73  972  pm2.74  973  pm2.82  974  moeq3  3708  unss1  4179  ordtri2or2  6463  gchor  10621  relin01  11737  icombl  25080  ioombl  25081  coltr  27895  frgrregorufrg  29576  cycpmco2  32287  fmlasuc  34372  satffunlem1lem2  34389  satffunlem2lem2  34392  naim1  35269  onsucconni  35317  dnibndlem13  35361  mblfinlem2  36521  leat3  38160  meetat2  38162  paddss1  38683  onov0suclim  42014  dflim5  42069  ordsssucim  42143