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	|- ( 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 331	1 |- ( ph -> ( ( th /\ ps ) -> ( th /\ ch ) ) )

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  1797  ssel  3057  sscon  3176  uniss  3723  trel3  3994  copsexg  4126  ssopab2  4157  coss1  4654  fununi  5149  imadif  5161  fss  5242  ssimaex  5436  opabbrex  5769  ssoprab2  5781  poxp  6083  pmss12g  6523  ss2ixp  6559  xpdom2  6678  qbtwnxr  9928  ioc0  9933  climshftlemg  10963  bezoutlembz  11538  tgcl  12076  neipsm  12166  ssnei2  12169  tgcnp  12220  cnpnei  12230  cnptopco  12233  mopni3  12473  limcresi  12591  cnlimcim  12596