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  601  exdistrfor  1849  mopick2  2166  ssrexf  3304  ssrexv  3307  ssdif  3358  ssrin  3450  reupick  3509  disjss1  4096  copsexg  4365  po3nr  4436  coss2  4916  fununi  5429  fiintim  7204  recexprlemlol  7957  recexprlemupu  7959  icoshft  10342  2ffzeq  10497  qbtwnxr  10641  ico0  10645  r19.2uz  11703  bezoutlemzz  12723  bezoutlemaz  12724  ptex  13561  rnglidlmmgm  14770  neiss  15141  uptx  15265  txcn  15266  bj-charfundcALT  16705