Theorem anim2i 340

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sylanl2  401  sylanr2  403  andi  808  pm4.55dc  923  xoranor  1356  19.41h  1664  sbimi  1738  equs5e  1768  exdistrfor  1773  equs45f  1775  sbidm  1824  eu3h  2045  eupickb  2081  2exeu  2092  darii  2100  festino  2106  baroco  2107  r19.27v  2562  r19.27av  2570  rspc2ev  2808  reu3  2878  difdif  3206  ssddif  3315  inssdif  3317  difin  3318  difindiss  3335  indifdir  3337  difrab  3355  iundif2ss  3886  trssord  4310  ordsuc  4486  find  4521  imainss  4962  dffun5r  5143  fof  5353  f1ocnv  5388  fv3  5452  relelfvdm  5461  funimass4  5480  fvelimab  5485  funconstss  5546  dff2  5572  dffo5  5577  dff1o6  5685  oprabid  5811  ssoprab2i  5868  releldm2  6091  ixpf  6622  recexgt0sr  7605  map2psrprg  7637  lediv2a  8677  lbreu  8727  elfzp12  9910  focdmex  10565  fihashf1rn  10567  cau3lem  10918  fsumcl2lem  11199  dvdsnegb  11546  dvds2add  11563  dvds2sub  11564  ndvdssub  11663  gcd2n0cl  11694  divgcdcoprmex  11819  cncongr1  11820  ctinfom  11977  istopfin  12206  toponcom  12233  cnptoprest  12447