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  1896  ssel  3242  sscon  3363  ifeqeqxdc  3687  uniss  3954  trel3  4235  copsexg  4382  ssopab2  4416  coss1  4933  fununi  5447  imadif  5459  fss  5544  ssimaex  5761  opabbrex  6126  ssoprab2  6138  poxp  6462  pmss12g  6950  ss2ixp  6987  xpdom2  7123  qbtwnxr  10675  ioc0  10680  climshftlemg  12051  bezoutlembz  12764  tgcl  15148  neipsm  15238  ssnei2  15241  tgcnp  15293  cnpnei  15303  cnptopco  15306  mopni3  15568  limcresi  15750  cnlimcim  15755