Theorem orim2d 881

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 24	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		orim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	orim12d 879	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ∨ wo 382

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 196  df-or 384  df-an 385

This theorem is referenced by:  orim2  882  pm2.82  893  poxp  7176  soxp  7177  relin01  10431  nneo  11337  uzp1  11597  vdwlem9  15531  dfcon2  21032  fin1aufil  21546  dgrlt  23826  aalioulem2  23892  aalioulem5  23895  aalioulem6  23896  aaliou  23897  sqff1o  24708  disjpreima  28779  disjdsct  28863  voliune  29619  volfiniune  29620  naim2  31555  paddss2  34122  lzunuz  36349  acongneg2  36562  nneom  42115