Theorem anim2i 340

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  401  sylanr2  403  andi  808  pm4.55dc  928  xoranor  1367  19.41h  1673  sbimi  1752  equs5e  1783  exdistrfor  1788  equs45f  1790  sbidm  1839  eu3h  2059  eupickb  2095  2exeu  2106  darii  2114  festino  2120  baroco  2121  r19.27v  2593  r19.27av  2601  rspc2ev  2845  reu3  2916  difdif  3247  ssddif  3356  inssdif  3358  difin  3359  difindiss  3376  indifdir  3378  difrab  3396  iundif2ss  3931  trssord  4358  ordsuc  4540  find  4576  imainss  5019  dffun5r  5200  fof  5410  f1ocnv  5445  fv3  5509  relelfvdm  5518  funimass4  5537  fvelimab  5542  funconstss  5603  dff2  5629  dffo5  5634  dff1o6  5744  oprabid  5874  ssoprab2i  5931  releldm2  6153  ixpf  6686  recexgt0sr  7714  map2psrprg  7746  lediv2a  8790  lbreu  8840  elfzp12  10034  focdmex  10700  fihashf1rn  10702  cau3lem  11056  fsumcl2lem  11339  dvdsnegb  11748  dvds2add  11765  dvds2sub  11766  ndvdssub  11867  gcd2n0cl  11902  divgcdcoprmex  12034  cncongr1  12035  ctinfom  12361  istopfin  12638  toponcom  12665  cnptoprest  12879