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  592  exdistrfor  1793  mopick2  2102  ssrexf  3209  ssrexv  3212  ssdif  3262  ssrin  3352  reupick  3411  disjss1  3972  copsexg  4229  po3nr  4295  coss2  4767  fununi  5266  fiintim  6906  recexprlemlol  7588  recexprlemupu  7590  icoshft  9947  2ffzeq  10097  qbtwnxr  10214  ico0  10218  r19.2uz  10957  bezoutlemzz  11957  bezoutlemaz  11958  neiss  12944  uptx  13068  txcn  13069  bj-charfundcALT  13844