Theorem anim2i 342

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

Proof of Theorem anim2i

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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  sylanl2  403  sylanr2  405  andi  826  xoranor  1422  19.41h  1733  sbimi  1812  equs5e  1843  exdistrfor  1848  equs45f  1850  sbidm  1899  eu3h  2125  eupickb  2161  2exeu  2172  darii  2180  festino  2186  baroco  2187  r19.27v  2661  r19.27av  2669  rspc2ev  2926  reu3  2997  difdif  3334  ssddif  3443  inssdif  3445  difin  3446  difindiss  3463  indifdir  3465  difrab  3483  iundif2ss  4041  trssord  4483  ordsuc  4667  find  4703  imainss  5159  dffun5r  5345  fof  5568  f1ocnv  5605  fv3  5671  relelfvdm  5680  funimass4  5705  fvelimab  5711  funconstss  5774  dff2  5799  dffo5  5804  dff1o6  5927  oprabid  6060  ssoprab2i  6120  uchoice  6309  releldm2  6357  ixpf  6932  recexgt0sr  8036  map2psrprg  8068  lediv2a  9117  lbreu  9167  elfzp12  10379  fihashf1rn  11096  ccatsymb  11228  swrdpfx  11337  pfxpfx  11338  pfxccatin12  11363  cau3lem  11737  fsumcl2lem  12022  dvdsnegb  12432  dvds2add  12449  dvds2sub  12450  ndvdssub  12554  gcd2n0cl  12603  divgcdcoprmex  12737  cncongr1  12738  ctinfom  13112  qusecsub  13981  istopfin  14794  toponcom  14821  cnptoprest  15033  dvmptfsum  15519  elply2  15529  subupgr  16197  uspgr2wlkeqi  16291  clwwlknun  16365