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

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  1891  ssel  3222  sscon  3343  uniss  3919  trel3  4200  copsexg  4342  ssopab2  4376  coss1  4891  fununi  5405  imadif  5417  fss  5501  ssimaex  5716  opabbrex  6075  ssoprab2  6087  poxp  6406  pmss12g  6887  ss2ixp  6923  xpdom2  7058  qbtwnxr  10563  ioc0  10568  climshftlemg  11925  bezoutlembz  12638  tgcl  14858  neipsm  14948  ssnei2  14951  tgcnp  15003  cnpnei  15013  cnptopco  15016  mopni3  15278  limcresi  15460  cnlimcim  15465