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  3236  sscon  3357  ifeqeqxdc  3673  uniss  3940  trel3  4221  copsexg  4365  ssopab2  4399  coss1  4915  fununi  5429  imadif  5441  fss  5526  ssimaex  5743  opabbrex  6105  ssoprab2  6117  poxp  6441  pmss12g  6922  ss2ixp  6959  xpdom2  7095  qbtwnxr  10644  ioc0  10649  climshftlemg  12015  bezoutlembz  12728  tgcl  15058  neipsm  15148  ssnei2  15151  tgcnp  15203  cnpnei  15213  cnptopco  15216  mopni3  15478  limcresi  15660  cnlimcim  15665