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  764  pm4.55dc  879  xoranor  1308  19.41h  1615  sbimi  1687  equs5e  1716  exdistrfor  1721  equs45f  1723  sbidm  1772  eu3h  1986  eupickb  2022  2exeu  2033  darii  2041  festino  2047  baroco  2048  r19.27av  2492  rspc2ev  2715  reu3  2782  difdif  3097  ssddif  3198  inssdif  3200  difin  3201  difindiss  3218  indifdir  3220  difrab  3238  iundif2ss  3743  trssord  4135  ordsuc  4306  find  4340  imainss  4759  dffun5r  4934  fof  5126  f1ocnv  5159  fv3  5218  relelfvdm  5226  funimass4  5245  fvelimab  5250  funconstss  5306  dff2  5332  dffo5  5337  dff1o6  5436  oprabid  5557  ssoprab2i  5613  releldm2  5831  recexgt0sr  6950  lediv2a  7973  lbreu  8023  elfzp12  9116  cau3lem  10000  dvdsnegb  10212  dvds2add  10229  dvds2sub  10230  ndvdssub  10330  gcd2n0cl  10361  divgcdcoprmex  10484  cncongr1  10485