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  820  xoranor  1397  19.41h  1709  sbimi  1788  equs5e  1819  exdistrfor  1824  equs45f  1826  sbidm  1875  eu3h  2101  eupickb  2137  2exeu  2148  darii  2156  festino  2162  baroco  2163  r19.27v  2635  r19.27av  2643  rspc2ev  2899  reu3  2970  difdif  3306  ssddif  3415  inssdif  3417  difin  3418  difindiss  3435  indifdir  3437  difrab  3455  iundif2ss  4007  trssord  4445  ordsuc  4629  find  4665  imainss  5117  dffun5r  5302  fof  5520  f1ocnv  5557  fv3  5622  relelfvdm  5631  funimass4  5652  fvelimab  5658  funconstss  5721  dff2  5747  dffo5  5752  dff1o6  5868  oprabid  5999  ssoprab2i  6057  uchoice  6246  releldm2  6294  ixpf  6830  recexgt0sr  7921  map2psrprg  7953  lediv2a  9003  lbreu  9053  elfzp12  10256  fihashf1rn  10970  ccatsymb  11096  swrdpfx  11198  pfxpfx  11199  pfxccatin12  11224  cau3lem  11540  fsumcl2lem  11824  dvdsnegb  12234  dvds2add  12251  dvds2sub  12252  ndvdssub  12356  gcd2n0cl  12405  divgcdcoprmex  12539  cncongr1  12540  ctinfom  12914  qusecsub  13782  istopfin  14587  toponcom  14614  cnptoprest  14826  dvmptfsum  15312  elply2  15322