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  5916  oprabid  6049  ssoprab2i  6109  uchoice  6299  releldm2  6347  ixpf  6888  recexgt0sr  7992  map2psrprg  8024  lediv2a  9074  lbreu  9124  elfzp12  10333  fihashf1rn  11049  ccatsymb  11178  swrdpfx  11287  pfxpfx  11288  pfxccatin12  11313  cau3lem  11674  fsumcl2lem  11958  dvdsnegb  12368  dvds2add  12385  dvds2sub  12386  ndvdssub  12490  gcd2n0cl  12539  divgcdcoprmex  12673  cncongr1  12674  ctinfom  13048  qusecsub  13917  istopfin  14723  toponcom  14750  cnptoprest  14962  dvmptfsum  15448  elply2  15458  subupgr  16123  uspgr2wlkeqi  16217  clwwlknun  16291