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  3236  sscon  3357  ifeqeqxdc  3673  uniss  3940  trel3  4221  copsexg  4365  ssopab2  4399  coss1  4915  fununi  5429  imadif  5441  fss  5526  ssimaex  5743  opabbrex  6105  ssoprab2  6117  poxp  6441  pmss12g  6922  ss2ixp  6959  xpdom2  7095  qbtwnxr  10641  ioc0  10646  climshftlemg  12012  bezoutlembz  12725  tgcl  15055  neipsm  15145  ssnei2  15148  tgcnp  15200  cnpnei  15210  cnptopco  15213  mopni3  15475  limcresi  15657  cnlimcim  15662