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  823  xoranor  1419  19.41h  1731  sbimi  1810  equs5e  1841  exdistrfor  1846  equs45f  1848  sbidm  1897  eu3h  2123  eupickb  2159  2exeu  2170  darii  2178  festino  2184  baroco  2185  r19.27v  2658  r19.27av  2666  rspc2ev  2922  reu3  2993  difdif  3329  ssddif  3438  inssdif  3440  difin  3441  difindiss  3458  indifdir  3460  difrab  3478  iundif2ss  4030  trssord  4470  ordsuc  4654  find  4690  imainss  5143  dffun5r  5329  fof  5547  f1ocnv  5584  fv3  5649  relelfvdm  5658  funimass4  5683  fvelimab  5689  funconstss  5752  dff2  5778  dffo5  5783  dff1o6  5899  oprabid  6032  ssoprab2i  6092  uchoice  6281  releldm2  6329  ixpf  6865  recexgt0sr  7956  map2psrprg  7988  lediv2a  9038  lbreu  9088  elfzp12  10291  fihashf1rn  11005  ccatsymb  11132  swrdpfx  11234  pfxpfx  11235  pfxccatin12  11260  cau3lem  11620  fsumcl2lem  11904  dvdsnegb  12314  dvds2add  12331  dvds2sub  12332  ndvdssub  12436  gcd2n0cl  12485  divgcdcoprmex  12619  cncongr1  12620  ctinfom  12994  qusecsub  13863  istopfin  14668  toponcom  14695  cnptoprest  14907  dvmptfsum  15393  elply2  15403