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  400  sylanr1  402  mpan10  466  sbcof2  1798  sbidm  1839  disamis  2125  r19.28v  2594  fun11uni  5258  fabexg  5375  fores  5419  f1oabexg  5444  fun11iun  5453  fvelrnb  5534  ssimaex  5547  foeqcnvco  5758  f1eqcocnv  5759  isoini  5786  brtposg  6222  tfrcllemssrecs  6320  fiintim  6894  djuex  7008  elni2  7255  dmaddpqlem  7318  nqpi  7319  ltexnqq  7349  nq0nn  7383  nqnq0a  7395  nqnq0m  7396  elnp1st2nd  7417  mullocprlem  7511  cnegexlem3  8075  divmulasscomap  8592  lediv2a  8790  btwnz  9310  eluz2b2  9541  uz2mulcl  9546  eqreznegel  9552  elioo4g  9870  fz0fzelfz0  10062  fz0fzdiffz0  10065  2ffzeq  10076  elfzodifsumelfzo  10136  elfzom1elp1fzo  10137  zpnn0elfzo  10142  ioo0  10195  zmodidfzoimp  10289  expcl2lemap  10467  mulreap  10806  redivap  10816  imdivap  10823  caucvgrelemcau  10922  zproddc  11520  fprodseq  11524  p1modz1  11734  negdvdsb  11747  muldvds1  11756  muldvds2  11757  dvdsdivcl  11788  nn0ehalf  11840  nn0oddm1d2  11846  nnoddm1d2  11847  infssuzex  11882  divgcdnn  11908  coprmgcdb  12020  divgcdcoprm0  12033  pw2dvdslemn  12097  oddprmdvds  12284  lgsprme0  13583