Theorem anim2d 335

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  spsbim  1820  ssel  3118  sscon  3237  uniss  3789  trel3  4066  copsexg  4199  ssopab2  4230  coss1  4734  fununi  5231  imadif  5243  fss  5324  ssimaex  5522  opabbrex  5855  ssoprab2  5867  poxp  6169  pmss12g  6609  ss2ixp  6645  xpdom2  6765  qbtwnxr  10135  ioc0  10140  climshftlemg  11176  bezoutlembz  11859  tgcl  12403  neipsm  12493  ssnei2  12496  tgcnp  12548  cnpnei  12558  cnptopco  12561  mopni3  12823  limcresi  12974  cnlimcim  12979