Theorem anim1d 329

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

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm3.45  561  exdistrfor  1721  mopick2  2024  ssrexv  3059  ssdif  3107  ssrin  3191  reupick  3248  disjss1  3772  copsexg  3999  po3nr  4065  coss2  4510  fununi  4987  recexprlemlol  6816  recexprlemupu  6818  icoshft  9012  2ffzeq  9151  qbtwnxr  9266  ico0  9270  r19.2uz  9879  bezoutlemzz  10391  bezoutlemaz  10392