Theorem orim2d 968

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  orim2  969  pm2.82  977  poxp  8110  soxp  8111  relin01  11709  nneo  12625  uzp1  12841  vdwlem9  16967  dfconn2  23313  fin1aufil  23826  dgrlt  26179  aalioulem2  26248  aalioulem5  26251  aalioulem6  26252  aaliou  26253  sqff1o  27099  disjpreima  32520  disjdsct  32633  voliune  34226  volfiniune  34227  satfvsucsuc  35359  naim2  36385  paddss2  39819  lzunuz  42763  acongneg2  42973  nneom  48520