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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spsbim  1892  ssel  3234  sscon  3355  uniss  3937  trel3  4218  copsexg  4362  ssopab2  4396  coss1  4912  fununi  5426  imadif  5438  fss  5523  ssimaex  5740  opabbrex  6099  ssoprab2  6111  poxp  6430  pmss12g  6911  ss2ixp  6948  xpdom2  7084  qbtwnxr  10624  ioc0  10629  climshftlemg  11995  bezoutlembz  12708  tgcl  14978  neipsm  15068  ssnei2  15071  tgcnp  15123  cnpnei  15133  cnptopco  15136  mopni3  15398  limcresi  15580  cnlimcim  15585