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  1788  mopick2  2097  ssrexf  3204  ssrexv  3207  ssdif  3257  ssrin  3347  reupick  3406  disjss1  3965  copsexg  4222  po3nr  4288  coss2  4760  fununi  5256  fiintim  6894  recexprlemlol  7567  recexprlemupu  7569  icoshft  9926  2ffzeq  10076  qbtwnxr  10193  ico0  10197  r19.2uz  10935  bezoutlemzz  11935  bezoutlemaz  11936  neiss  12790  uptx  12914  txcn  12915  bj-charfundcALT  13691