Theorem anim2i 339

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 336	1 |- ( ( ch /\ ph ) -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylanl2  400  sylanr2  402  andi  807  pm4.55dc  922  xoranor  1355  19.41h  1663  sbimi  1737  equs5e  1767  exdistrfor  1772  equs45f  1774  sbidm  1823  eu3h  2044  eupickb  2080  2exeu  2091  darii  2099  festino  2105  baroco  2106  r19.27v  2559  r19.27av  2567  rspc2ev  2804  reu3  2874  difdif  3201  ssddif  3310  inssdif  3312  difin  3313  difindiss  3330  indifdir  3332  difrab  3350  iundif2ss  3878  trssord  4302  ordsuc  4478  find  4513  imainss  4954  dffun5r  5135  fof  5345  f1ocnv  5380  fv3  5444  relelfvdm  5453  funimass4  5472  fvelimab  5477  funconstss  5538  dff2  5564  dffo5  5569  dff1o6  5677  oprabid  5803  ssoprab2i  5860  releldm2  6083  ixpf  6614  recexgt0sr  7581  map2psrprg  7613  lediv2a  8653  lbreu  8703  elfzp12  9879  focdmex  10533  fihashf1rn  10535  cau3lem  10886  fsumcl2lem  11167  dvdsnegb  11510  dvds2add  11527  dvds2sub  11528  ndvdssub  11627  gcd2n0cl  11658  divgcdcoprmex  11783  cncongr1  11784  ctinfom  11941  istopfin  12167  toponcom  12194  cnptoprest  12408