Theorem anim2d 335

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

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  spsbim  1815  ssel  3086  sscon  3205  uniss  3752  trel3  4029  copsexg  4161  ssopab2  4192  coss1  4689  fununi  5186  imadif  5198  fss  5279  ssimaex  5475  opabbrex  5808  ssoprab2  5820  poxp  6122  pmss12g  6562  ss2ixp  6598  xpdom2  6718  qbtwnxr  10028  ioc0  10033  climshftlemg  11064  bezoutlembz  11681  tgcl  12222  neipsm  12312  ssnei2  12315  tgcnp  12367  cnpnei  12377  cnptopco  12380  mopni3  12642  limcresi  12793  cnlimcim  12798