Theorem orim2d 965

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 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 398  df-or 846

This theorem is referenced by:  orim2  966  pm2.82  974  poxp  8000  soxp  8001  relin01  11545  nneo  12450  uzp1  12665  vdwlem9  16735  dfconn2  22615  fin1aufil  23128  dgrlt  25472  aalioulem2  25538  aalioulem5  25541  aalioulem6  25542  aaliou  25543  sqff1o  26376  disjpreima  30968  disjdsct  31080  voliune  32242  volfiniune  32243  satfvsucsuc  33372  naim2  34624  paddss2  37874  lzunuz  40627  acongneg2  40837  nneom  45931