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  825  xoranor  1421  19.41h  1733  sbimi  1812  equs5e  1843  exdistrfor  1848  equs45f  1850  sbidm  1899  eu3h  2125  eupickb  2161  2exeu  2172  darii  2180  festino  2186  baroco  2187  r19.27v  2660  r19.27av  2668  rspc2ev  2925  reu3  2996  difdif  3332  ssddif  3441  inssdif  3443  difin  3444  difindiss  3461  indifdir  3463  difrab  3481  iundif2ss  4036  trssord  4477  ordsuc  4661  find  4697  imainss  5152  dffun5r  5338  fof  5559  f1ocnv  5596  fv3  5662  relelfvdm  5671  funimass4  5696  fvelimab  5702  funconstss  5765  dff2  5791  dffo5  5796  dff1o6  5917  oprabid  6050  ssoprab2i  6110  uchoice  6300  releldm2  6348  ixpf  6889  recexgt0sr  7993  map2psrprg  8025  lediv2a  9075  lbreu  9125  elfzp12  10334  fihashf1rn  11051  ccatsymb  11183  swrdpfx  11292  pfxpfx  11293  pfxccatin12  11318  cau3lem  11692  fsumcl2lem  11977  dvdsnegb  12387  dvds2add  12404  dvds2sub  12405  ndvdssub  12509  gcd2n0cl  12558  divgcdcoprmex  12692  cncongr1  12693  ctinfom  13067  qusecsub  13936  istopfin  14743  toponcom  14770  cnptoprest  14982  dvmptfsum  15468  elply2  15478  subupgr  16143  uspgr2wlkeqi  16237  clwwlknun  16311