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  1823  mopick2  2137  ssrexf  3255  ssrexv  3258  ssdif  3308  ssrin  3398  reupick  3457  disjss1  4027  copsexg  4288  po3nr  4357  coss2  4834  fununi  5342  fiintim  7028  recexprlemlol  7739  recexprlemupu  7741  icoshft  10112  2ffzeq  10263  qbtwnxr  10400  ico0  10404  r19.2uz  11304  bezoutlemzz  12323  bezoutlemaz  12324  ptex  13096  rnglidlmmgm  14258  neiss  14622  uptx  14746  txcn  14747  bj-charfundcALT  15745