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  1869  ssel  3198  sscon  3318  uniss  3888  trel3  4169  copsexg  4309  ssopab2  4343  coss1  4854  fununi  5365  imadif  5377  fss  5461  ssimaex  5668  opabbrex  6019  ssoprab2  6031  poxp  6348  pmss12g  6792  ss2ixp  6828  xpdom2  6958  qbtwnxr  10444  ioc0  10449  climshftlemg  11779  bezoutlembz  12491  tgcl  14703  neipsm  14793  ssnei2  14796  tgcnp  14848  cnpnei  14858  cnptopco  14861  mopni3  15123  limcresi  15305  cnlimcim  15310