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  3091  sscon  3210  uniss  3757  trel3  4034  copsexg  4166  ssopab2  4197  coss1  4694  fununi  5191  imadif  5203  fss  5284  ssimaex  5482  opabbrex  5815  ssoprab2  5827  poxp  6129  pmss12g  6569  ss2ixp  6605  xpdom2  6725  qbtwnxr  10035  ioc0  10040  climshftlemg  11071  bezoutlembz  11692  tgcl  12233  neipsm  12323  ssnei2  12326  tgcnp  12378  cnpnei  12388  cnptopco  12391  mopni3  12653  limcresi  12804  cnlimcim  12809