Theorem anim2d 333

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  spsbim  1795  ssel  3055  sscon  3174  uniss  3721  trel3  3992  copsexg  4124  ssopab2  4155  coss1  4652  fununi  5147  imadif  5159  fss  5240  ssimaex  5434  opabbrex  5767  ssoprab2  5779  poxp  6081  pmss12g  6521  ss2ixp  6557  xpdom2  6676  qbtwnxr  9922  ioc0  9927  climshftlemg  10957  bezoutlembz  11532  tgcl  12070  neipsm  12160  ssnei2  12163  tgcnp  12214  cnpnei  12224  cnptopco  12227  mopni3  12467  limcresi  12585  cnlimcim  12590