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  2923  reu3  2994  difdif  3330  ssddif  3439  inssdif  3441  difin  3442  difindiss  3459  indifdir  3461  difrab  3479  iundif2ss  4034  trssord  4475  ordsuc  4659  find  4695  imainss  5150  dffun5r  5336  fof  5556  f1ocnv  5593  fv3  5658  relelfvdm  5667  funimass4  5692  fvelimab  5698  funconstss  5761  dff2  5787  dffo5  5792  dff1o6  5912  oprabid  6045  ssoprab2i  6105  uchoice  6295  releldm2  6343  ixpf  6884  recexgt0sr  7983  map2psrprg  8015  lediv2a  9065  lbreu  9115  elfzp12  10324  fihashf1rn  11040  ccatsymb  11169  swrdpfx  11278  pfxpfx  11279  pfxccatin12  11304  cau3lem  11665  fsumcl2lem  11949  dvdsnegb  12359  dvds2add  12376  dvds2sub  12377  ndvdssub  12481  gcd2n0cl  12530  divgcdcoprmex  12664  cncongr1  12665  ctinfom  13039  qusecsub  13908  istopfin  14714  toponcom  14741  cnptoprest  14953  dvmptfsum  15439  elply2  15449  uspgr2wlkeqi  16164  clwwlknun  16236