Theorem anim1i 340

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1i.1	|- ( ph -> ps )

Assertion

Ref	Expression
anim1i	|- ( ( ph /\ ch ) -> ( ps /\ ch ) )

Proof of Theorem anim1i

Step	Hyp	Ref	Expression
1		anim1i.1	. 2 |- ( ph -> ps )
2		id 19	. 2 |- ( ch -> ch )
3	1, 2	anim12i 338	1 |- ( ( ph /\ ch ) -> ( ps /\ ch ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylanl1  406  sylanr1  408  mpan10  478  sbcof2  1863  sbidm  1904  disamis  2198  r19.28v  2679  fun11uni  5451  fabexg  5579  fores  5625  f1oabexg  5651  fun11iun  5660  fdmeu  5746  fvelrnb  5750  ssimaex  5764  foeqcnvco  5996  f1eqcocnv  5997  isoini  6024  brtposg  6525  tfrcllemssrecs  6623  fiintim  7238  djuex  7383  elni2  7681  dmaddpqlem  7744  nqpi  7745  ltexnqq  7775  nq0nn  7809  nqnq0a  7821  nqnq0m  7822  elnp1st2nd  7843  mullocprlem  7937  cnegexlem3  8504  divmulasscomap  9028  lediv2a  9227  btwnz  9769  eluz2b2  10012  uz2mulcl  10017  eqreznegel  10023  elioo4g  10346  fz0fzelfz0  10544  fz0fzdiffz0  10547  2ffzeq  10558  elfzodifsumelfzo  10629  elfzom1elp1fzo  10630  zpnn0elfzo  10635  infssuzex  10676  ioo0  10704  zmodidfzoimp  10804  expcl2lemap  11001  hashfibclem  11296  iswrdsymb  11336  ccatcl  11375  ccatsymb  11384  swrdfv2  11449  swrdsbslen  11452  swrdspsleq  11453  pfxswrd  11492  pfxccatin12lem3  11518  pfxccatpfx2  11523  swrdccat3blem  11525  reuccatpfxs1  11533  mulreap  11643  redivap  11653  imdivap  11660  caucvgrelemcau  11760  zproddc  12362  fprodseq  12366  p1modz1  12577  negdvdsb  12590  muldvds1  12599  muldvds2  12600  dvdsdivcl  12633  nn0ehalf  12686  nn0oddm1d2  12692  nnoddm1d2  12693  divgcdnn  12768  coprmgcdb  12882  divgcdcoprm0  12895  pwbdvdslemn  12960  oddprmdvds  13153  4sqexercise1  13197  4sqexercise2  13198  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemth  13330  grpissubg  14046  ecqusaddd  14090  ecqusaddcl  14091  rnglz  14293  qusmulrng  14918  quscrng  14919  dvdsrzring  14987  bcmono  16202  lgsprme0  16259  gausslemma2dlem0e  16270  gausslemma2dlem1a  16275  gausslemma2dlem6  16284  lgsquadlem2  16295  2lgsoddprm  16330  usgrislfuspgrdom  16529  edgssv2en  16538  umgr2edg  16546  uspgredg2v  16560  subupgr  16612  subusgr  16614  vtxdfifiun  16636  eupth2lem3lem3fi  16809