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  1865  ssel  3186  sscon  3306  uniss  3870  trel3  4149  copsexg  4287  ssopab2  4320  coss1  4831  fununi  5336  imadif  5348  fss  5431  ssimaex  5634  opabbrex  5979  ssoprab2  5991  poxp  6308  pmss12g  6752  ss2ixp  6788  xpdom2  6908  qbtwnxr  10381  ioc0  10386  climshftlemg  11532  bezoutlembz  12244  tgcl  14454  neipsm  14544  ssnei2  14547  tgcnp  14599  cnpnei  14609  cnptopco  14612  mopni3  14874  limcresi  15056  cnlimcim  15061