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  407  sylanr2  409  andi  830  xoranor  1426  19.41h  1737  sbimi  1817  equs5e  1848  exdistrfor  1853  equs45f  1855  sbidm  1904  eu3h  2132  eupickb  2168  2exeu  2179  darii  2187  festino  2193  baroco  2194  r19.27v  2678  r19.27av  2686  rspc2ev  2945  reu3  3016  difdif  3354  ssddif  3465  inssdif  3467  difin  3468  difindiss  3485  indifdir  3487  difrab  3507  iundif2ss  4073  trssord  4520  ordsuc  4705  find  4741  imainss  5198  dffun5r  5384  fof  5610  f1ocnv  5647  fv3  5713  relelfvdm  5722  funimass4  5747  fvelimab  5753  funconstss  5818  dff2  5843  dffo5  5848  dff1o6  5972  oprabid  6107  ssoprab2i  6167  uchoice  6361  releldm2  6409  ixpf  6992  recexgt0sr  8130  map2psrprg  8162  lediv2a  9215  lbreu  9265  elfzp12  10484  fihashf1rn  11205  ccatsymb  11348  swrdpfx  11457  pfxpfx  11458  pfxccatin12  11483  cau3lem  11858  fsumcl2lem  12143  dvdsnegb  12553  dvds2add  12570  dvds2sub  12571  ndvdssub  12675  gcd2n0cl  12724  divgcdcoprmex  12858  cncongr1  12859  ballotfilemirc  13253  ctinfom  13297  qusecsub  14112  istopfin  15024  toponcom  15051  cnptoprest  15263  dvmptfsum  15749  elply2  15759  subupgr  16428  uspgr2wlkeqi  16522  clwwlknun  16596