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  586  exdistrfor  1772  mopick2  2082  ssrexf  3159  ssrexv  3162  ssdif  3211  ssrin  3301  reupick  3360  disjss1  3912  copsexg  4166  po3nr  4232  coss2  4695  fununi  5191  fiintim  6817  recexprlemlol  7437  recexprlemupu  7439  icoshft  9776  2ffzeq  9921  qbtwnxr  10038  ico0  10042  r19.2uz  10768  bezoutlemzz  11693  bezoutlemaz  11694  neiss  12322  uptx  12446  txcn  12447