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  587  exdistrfor  1773  mopick2  2083  ssrexf  3164  ssrexv  3167  ssdif  3216  ssrin  3306  reupick  3365  disjss1  3920  copsexg  4174  po3nr  4240  coss2  4703  fununi  5199  fiintim  6825  recexprlemlol  7458  recexprlemupu  7460  icoshft  9803  2ffzeq  9949  qbtwnxr  10066  ico0  10070  r19.2uz  10797  bezoutlemzz  11726  bezoutlemaz  11727  neiss  12358  uptx  12482  txcn  12483