Theorem anim1d 336

Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)

Hypothesis

Ref	Expression
anim1d.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
anim1d	|- ( ph -> ( ( ps /\ th ) -> ( ch /\ th ) ) )

Proof of Theorem anim1d

Step	Hyp	Ref	Expression
1		anim1d.1	. 2 |- ( ph -> ( ps -> ch ) )
2		idd 21	. 2 |- ( ph -> ( th -> th ) )
3	1, 2	anim12d 335	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ th ) ) )

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:  pm3.45  597  exdistrfor  1824  mopick2  2139  ssrexf  3263  ssrexv  3266  ssdif  3316  ssrin  3406  reupick  3465  disjss1  4041  copsexg  4306  po3nr  4375  coss2  4852  fununi  5361  fiintim  7054  recexprlemlol  7774  recexprlemupu  7776  icoshft  10147  2ffzeq  10298  qbtwnxr  10437  ico0  10441  r19.2uz  11419  bezoutlemzz  12438  bezoutlemaz  12439  ptex  13211  rnglidlmmgm  14373  neiss  14737  uptx  14861  txcn  14862  bj-charfundcALT  15944