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  605  exdistrfor  1853  mopick2  2170  ssrexf  3310  ssrexv  3313  ssdif  3364  ssrin  3456  reupick  3517  disjss1  4107  copsexg  4379  po3nr  4450  coss2  4931  fununi  5444  fiintim  7228  recexprlemlol  7983  recexprlemupu  7985  icoshft  10371  2ffzeq  10526  qbtwnxr  10670  ico0  10674  r19.2uz  11737  bezoutlemzz  12757  bezoutlemaz  12758  ptex  13595  rnglidlmmgm  14805  neiss  15174  uptx  15298  txcn  15299  bj-charfundcALT  16749