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  7384  elni2  7682  dmaddpqlem  7745  nqpi  7746  ltexnqq  7776  nq0nn  7810  nqnq0a  7822  nqnq0m  7823  elnp1st2nd  7844  mullocprlem  7938  cnegexlem3  8505  divmulasscomap  9029  lediv2a  9228  btwnz  9770  eluz2b2  10013  uz2mulcl  10018  eqreznegel  10024  elioo4g  10347  fz0fzelfz0  10545  fz0fzdiffz0  10548  2ffzeq  10559  elfzodifsumelfzo  10630  elfzom1elp1fzo  10631  zpnn0elfzo  10636  infssuzex  10677  ioo0  10705  zmodidfzoimp  10806  expcl2lemap  11003  hashfibclem  11298  iswrdsymb  11338  ccatcl  11377  ccatsymb  11386  swrdfv2  11451  swrdsbslen  11454  swrdspsleq  11455  pfxswrd  11494  pfxccatin12lem3  11520  pfxccatpfx2  11525  swrdccat3blem  11527  reuccatpfxs1  11535  mulreap  11645  redivap  11655  imdivap  11662  caucvgrelemcau  11762  zproddc  12365  fprodseq  12369  p1modz1  12580  negdvdsb  12593  muldvds1  12602  muldvds2  12603  dvdsdivcl  12636  nn0ehalf  12689  nn0oddm1d2  12695  nnoddm1d2  12696  divgcdnn  12771  coprmgcdb  12885  divgcdcoprm0  12898  pwbdvdslemn  12963  oddprmdvds  13156  4sqexercise1  13200  4sqexercise2  13201  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemth  13333  grpissubg  14050  ecqusaddd  14094  ecqusaddcl  14095  rnglz  14328  qusmulrng  14953  quscrng  14954  dvdsrzring  15022  bcmono  16265  lgsprme0  16327  gausslemma2dlem0e  16338  gausslemma2dlem1a  16343  gausslemma2dlem6  16352  lgsquadlem2  16363  2lgsoddprm  16398  usgrislfuspgrdom  16597  edgssv2en  16606  umgr2edg  16614  uspgredg2v  16628  subupgr  16680  subusgr  16682  vtxdfifiun  16704  eupth2lem3lem3fi  16877