Theorem anim1d 334

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 333	1 |- ( ph -> ( ( ps /\ th ) -> ( ch /\ th ) ) )

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:  pm3.45  587  exdistrfor  1780  mopick2  2089  ssrexf  3190  ssrexv  3193  ssdif  3242  ssrin  3332  reupick  3391  disjss1  3948  copsexg  4203  po3nr  4269  coss2  4739  fununi  5235  fiintim  6866  recexprlemlol  7529  recexprlemupu  7531  icoshft  9876  2ffzeq  10022  qbtwnxr  10139  ico0  10143  r19.2uz  10875  bezoutlemzz  11866  bezoutlemaz  11867  neiss  12510  uptx  12634  txcn  12635  bj-charfundcALT  13343