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  10366  ioc0  10371  climshftlemg  11486  bezoutlembz  12198  tgcl  14408  neipsm  14498  ssnei2  14501  tgcnp  14553  cnpnei  14563  cnptopco  14566  mopni3  14828  limcresi  15010  cnlimcim  15015