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	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
anim2d	|- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 21	. 2 |- ( ph -> ( th -> th ) )
2		anim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	anim12d 333	1 |- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

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  1831  ssel  3136  sscon  3256  uniss  3810  trel3  4088  copsexg  4222  ssopab2  4253  coss1  4759  fununi  5256  imadif  5268  fss  5349  ssimaex  5547  opabbrex  5886  ssoprab2  5898  poxp  6200  pmss12g  6641  ss2ixp  6677  xpdom2  6797  qbtwnxr  10193  ioc0  10198  climshftlemg  11243  bezoutlembz  11937  tgcl  12704  neipsm  12794  ssnei2  12797  tgcnp  12849  cnpnei  12859  cnptopco  12862  mopni3  13124  limcresi  13275  cnlimcim  13280