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  1857  ssel  3178  sscon  3298  uniss  3861  trel3  4140  copsexg  4278  ssopab2  4311  coss1  4822  fununi  5327  imadif  5339  fss  5422  ssimaex  5625  opabbrex  5970  ssoprab2  5982  poxp  6299  pmss12g  6743  ss2ixp  6779  xpdom2  6899  qbtwnxr  10364  ioc0  10369  climshftlemg  11484  bezoutlembz  12196  tgcl  14384  neipsm  14474  ssnei2  14477  tgcnp  14529  cnpnei  14539  cnptopco  14542  mopni3  14804  limcresi  14986  cnlimcim  14991