Theorem orim2d 778

Description: Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)

Hypothesis

Ref	Expression
orim1d.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
orim2d	⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

Proof of Theorem orim2d

Step	Hyp	Ref	Expression
1		idd 21	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		orim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	orim12d 776	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orim2  779  orbi2d  780  pm2.82  802  stdcndcOLD  832  pm2.13dc  871  exmid1dc  4131  acexmidlemcase  5777  poxp  6137  fodjuomnilemdc  7024  omniwomnimkv  7049  indpi  7174  suplocexprlemloc  7553  nneoor  9177  uzp1  9383  maxabslemlub  11011  xrmaxiflemlub  11049  exmidunben  11975  bj-nn0suc  13333  sbthomlem  13395