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  1867  ssel  3191  sscon  3311  uniss  3877  trel3  4158  copsexg  4296  ssopab2  4330  coss1  4841  fununi  5351  imadif  5363  fss  5447  ssimaex  5653  opabbrex  6002  ssoprab2  6014  poxp  6331  pmss12g  6775  ss2ixp  6811  xpdom2  6941  qbtwnxr  10422  ioc0  10427  climshftlemg  11688  bezoutlembz  12400  tgcl  14611  neipsm  14701  ssnei2  14704  tgcnp  14756  cnpnei  14766  cnptopco  14769  mopni3  15031  limcresi  15213  cnlimcim  15218