Theorem orim2d 967

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  orim2  968  pm2.82  976  poxp  8169  soxp  8170  relin01  11814  nneo  12727  uzp1  12944  vdwlem9  17036  dfconn2  23448  fin1aufil  23961  dgrlt  26326  aalioulem2  26393  aalioulem5  26396  aalioulem6  26397  aaliou  26398  sqff1o  27243  disjpreima  32606  disjdsct  32714  voliune  34193  volfiniune  34194  satfvsucsuc  35333  naim2  36356  paddss2  39775  lzunuz  42724  acongneg2  42934  nneom  48261