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  1836  ssel  3141  sscon  3261  uniss  3817  trel3  4095  copsexg  4229  ssopab2  4260  coss1  4766  fununi  5266  imadif  5278  fss  5359  ssimaex  5557  opabbrex  5897  ssoprab2  5909  poxp  6211  pmss12g  6653  ss2ixp  6689  xpdom2  6809  qbtwnxr  10214  ioc0  10219  climshftlemg  11265  bezoutlembz  11959  tgcl  12858  neipsm  12948  ssnei2  12951  tgcnp  13003  cnpnei  13013  cnptopco  13016  mopni3  13278  limcresi  13429  cnlimcim  13434