Theorem anim1i 338

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 336	1 |- ( ( ph /\ ch ) -> ( ps /\ ch ) )

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 is referenced by:  sylanl1  399  sylanr1  401  mpan10  465  sbcof2  1782  sbidm  1823  disamis  2110  r19.28v  2560  fun11uni  5193  fabexg  5310  fores  5354  f1oabexg  5379  fun11iun  5388  fvelrnb  5469  ssimaex  5482  foeqcnvco  5691  f1eqcocnv  5692  isoini  5719  brtposg  6151  tfrcllemssrecs  6249  fiintim  6817  djuex  6928  elni2  7125  dmaddpqlem  7188  nqpi  7189  ltexnqq  7219  nq0nn  7253  nqnq0a  7265  nqnq0m  7266  elnp1st2nd  7287  mullocprlem  7381  cnegexlem3  7942  divmulasscomap  8459  lediv2a  8656  btwnz  9173  eluz2b2  9400  uz2mulcl  9405  eqreznegel  9409  elioo4g  9720  fz0fzelfz0  9907  fz0fzdiffz0  9910  2ffzeq  9921  elfzodifsumelfzo  9981  elfzom1elp1fzo  9982  zpnn0elfzo  9987  ioo0  10040  zmodidfzoimp  10130  expcl2lemap  10308  mulreap  10639  redivap  10649  imdivap  10656  caucvgrelemcau  10755  negdvdsb  11512  muldvds1  11521  muldvds2  11522  dvdsdivcl  11551  nn0ehalf  11603  nn0oddm1d2  11609  nnoddm1d2  11610  infssuzex  11645  divgcdnn  11666  coprmgcdb  11772  divgcdcoprm0  11785  pw2dvdslemn  11846