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  3241  ssrexv  3244  ssdif  3294  ssrin  3384  reupick  3443  disjss1  4012  copsexg  4273  po3nr  4341  coss2  4818  fununi  5322  fiintim  6985  recexprlemlol  7686  recexprlemupu  7688  icoshft  10056  2ffzeq  10207  qbtwnxr  10326  ico0  10330  r19.2uz  11137  bezoutlemzz  12139  bezoutlemaz  12140  ptex  12875  rnglidlmmgm  13992  neiss  14318  uptx  14442  txcn  14443  bj-charfundcALT  15301