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  1813  equs5e  1844  exdistrfor  1849  equs45f  1851  sbidm  1900  eu3h  2128  eupickb  2164  2exeu  2175  darii  2183  festino  2189  baroco  2190  r19.27v  2672  r19.27av  2680  rspc2ev  2939  reu3  3010  difdif  3348  ssddif  3459  inssdif  3461  difin  3462  difindiss  3479  indifdir  3481  difrab  3499  iundif2ss  4062  trssord  4506  ordsuc  4690  find  4726  imainss  5183  dffun5r  5369  fof  5595  f1ocnv  5632  fv3  5698  relelfvdm  5707  funimass4  5732  fvelimab  5738  funconstss  5801  dff2  5826  dffo5  5831  dff1o6  5955  oprabid  6090  ssoprab2i  6150  uchoice  6344  releldm2  6392  ixpf  6968  recexgt0sr  8104  map2psrprg  8136  lediv2a  9186  lbreu  9236  elfzp12  10455  fihashf1rn  11176  ccatsymb  11315  swrdpfx  11424  pfxpfx  11425  pfxccatin12  11450  cau3lem  11824  fsumcl2lem  12109  dvdsnegb  12519  dvds2add  12536  dvds2sub  12537  ndvdssub  12641  gcd2n0cl  12690  divgcdcoprmex  12824  cncongr1  12825  ballotfilemirc  13219  ctinfom  13263  qusecsub  14084  istopfin  14991  toponcom  15018  cnptoprest  15230  dvmptfsum  15716  elply2  15726  subupgr  16394  uspgr2wlkeqi  16488  clwwlknun  16562