Theorem anim2i 334

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  sylanl2  395  sylanr2  397  andi  765  pm4.55dc  880  xoranor  1309  19.41h  1616  sbimi  1688  equs5e  1717  exdistrfor  1722  equs45f  1724  sbidm  1773  eu3h  1987  eupickb  2023  2exeu  2034  darii  2042  festino  2048  baroco  2049  r19.27av  2493  rspc2ev  2716  reu3  2783  difdif  3098  ssddif  3205  inssdif  3207  difin  3208  difindiss  3225  indifdir  3227  difrab  3245  iundif2ss  3751  trssord  4143  ordsuc  4314  find  4348  imainss  4769  dffun5r  4944  fof  5137  f1ocnv  5170  fv3  5229  relelfvdm  5237  funimass4  5256  fvelimab  5261  funconstss  5317  dff2  5343  dffo5  5348  dff1o6  5447  oprabid  5568  ssoprab2i  5624  releldm2  5842  recexgt0sr  7012  lediv2a  8040  lbreu  8090  elfzp12  9192  focdmex  9811  sizef1rn  9813  cau3lem  10138  dvdsnegb  10357  dvds2add  10374  dvds2sub  10375  ndvdssub  10474  gcd2n0cl  10505  divgcdcoprmex  10628  cncongr1  10629