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  1854  ssel  3174  sscon  3294  uniss  3857  trel3  4136  copsexg  4274  ssopab2  4307  coss1  4818  fununi  5323  imadif  5335  fss  5416  ssimaex  5619  opabbrex  5963  ssoprab2  5975  poxp  6287  pmss12g  6731  ss2ixp  6767  xpdom2  6887  qbtwnxr  10329  ioc0  10334  climshftlemg  11448  bezoutlembz  12144  tgcl  14243  neipsm  14333  ssnei2  14336  tgcnp  14388  cnpnei  14398  cnptopco  14401  mopni3  14663  limcresi  14845  cnlimcim  14850