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  1708  sbimi  1787  equs5e  1818  exdistrfor  1823  equs45f  1825  sbidm  1874  eu3h  2099  eupickb  2135  2exeu  2146  darii  2154  festino  2160  baroco  2161  r19.27v  2633  r19.27av  2641  rspc2ev  2892  reu3  2963  difdif  3298  ssddif  3407  inssdif  3409  difin  3410  difindiss  3427  indifdir  3429  difrab  3447  iundif2ss  3993  trssord  4427  ordsuc  4611  find  4647  imainss  5098  dffun5r  5283  fof  5498  f1ocnv  5535  fv3  5599  relelfvdm  5608  funimass4  5629  fvelimab  5635  funconstss  5698  dff2  5724  dffo5  5729  dff1o6  5845  oprabid  5976  ssoprab2i  6034  uchoice  6223  releldm2  6271  ixpf  6807  recexgt0sr  7886  map2psrprg  7918  lediv2a  8968  lbreu  9018  elfzp12  10221  fihashf1rn  10933  ccatsymb  11058  cau3lem  11425  fsumcl2lem  11709  dvdsnegb  12119  dvds2add  12136  dvds2sub  12137  ndvdssub  12241  gcd2n0cl  12290  divgcdcoprmex  12424  cncongr1  12425  ctinfom  12799  qusecsub  13667  istopfin  14472  toponcom  14499  cnptoprest  14711  dvmptfsum  15197  elply2  15207