Theorem anim2d 337

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
anim2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 21	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
2		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	anim12d 335	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  spsbim  1896  ssel  3242  sscon  3363  ifeqeqxdc  3687  uniss  3956  trel3  4239  copsexg  4386  ssopab2  4420  coss1  4937  fununi  5452  imadif  5464  fss  5549  ssimaex  5767  opabbrex  6135  ssoprab2  6147  poxp  6472  pmss12g  6960  ss2ixp  6998  xpdom2  7134  qbtwnxr  10710  ioc0  10715  climshftlemg  12094  bezoutlembz  12807  tgcl  15302  neipsm  15392  ssnei2  15395  tgcnp  15447  cnpnei  15457  cnptopco  15460  mopni3  15722  limcresi  15904  cnlimcim  15909