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  1892  ssel  3232  sscon  3353  uniss  3935  trel3  4216  copsexg  4360  ssopab2  4394  coss1  4910  fununi  5424  imadif  5436  fss  5521  ssimaex  5738  opabbrex  6097  ssoprab2  6109  poxp  6428  pmss12g  6909  ss2ixp  6946  xpdom2  7082  qbtwnxr  10617  ioc0  10622  climshftlemg  11987  bezoutlembz  12700  tgcl  14929  neipsm  15019  ssnei2  15022  tgcnp  15074  cnpnei  15084  cnptopco  15087  mopni3  15349  limcresi  15531  cnlimcim  15536