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  2126  eupickb  2162  2exeu  2173  darii  2181  festino  2187  baroco  2188  r19.27v  2670  r19.27av  2678  rspc2ev  2936  reu3  3007  difdif  3344  ssddif  3455  inssdif  3457  difin  3458  difindiss  3475  indifdir  3477  difrab  3495  iundif2ss  4057  trssord  4501  ordsuc  4685  find  4721  imainss  5178  dffun5r  5364  fof  5590  f1ocnv  5627  fv3  5693  relelfvdm  5702  funimass4  5727  fvelimab  5733  funconstss  5796  dff2  5821  dffo5  5826  dff1o6  5949  oprabid  6082  ssoprab2i  6142  uchoice  6331  releldm2  6379  ixpf  6955  recexgt0sr  8088  map2psrprg  8120  lediv2a  9169  lbreu  9219  elfzp12  10433  fihashf1rn  11151  ccatsymb  11290  swrdpfx  11399  pfxpfx  11400  pfxccatin12  11425  cau3lem  11799  fsumcl2lem  12084  dvdsnegb  12494  dvds2add  12511  dvds2sub  12512  ndvdssub  12616  gcd2n0cl  12665  divgcdcoprmex  12799  cncongr1  12800  ctinfom  13179  qusecsub  14048  istopfin  14865  toponcom  14892  cnptoprest  15104  dvmptfsum  15590  elply2  15600  subupgr  16268  uspgr2wlkeqi  16362  clwwlknun  16436