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  1811  mopick2  2125  ssrexf  3242  ssrexv  3245  ssdif  3295  ssrin  3385  reupick  3444  disjss1  4013  copsexg  4274  po3nr  4342  coss2  4819  fununi  5323  fiintim  6987  recexprlemlol  7688  recexprlemupu  7690  icoshft  10059  2ffzeq  10210  qbtwnxr  10329  ico0  10333  r19.2uz  11140  bezoutlemzz  12142  bezoutlemaz  12143  ptex  12878  rnglidlmmgm  13995  neiss  14329  uptx  14453  txcn  14454  bj-charfundcALT  15371