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  819  xoranor  1396  19.41h  1707  sbimi  1786  equs5e  1817  exdistrfor  1822  equs45f  1824  sbidm  1873  eu3h  2098  eupickb  2134  2exeu  2145  darii  2153  festino  2159  baroco  2160  r19.27v  2632  r19.27av  2640  rspc2ev  2891  reu3  2962  difdif  3297  ssddif  3406  inssdif  3408  difin  3409  difindiss  3426  indifdir  3428  difrab  3446  iundif2ss  3992  trssord  4426  ordsuc  4610  find  4646  imainss  5097  dffun5r  5282  fof  5497  f1ocnv  5534  fv3  5598  relelfvdm  5607  funimass4  5628  fvelimab  5634  funconstss  5697  dff2  5723  dffo5  5728  dff1o6  5844  oprabid  5975  ssoprab2i  6033  uchoice  6222  releldm2  6270  ixpf  6806  recexgt0sr  7885  map2psrprg  7917  lediv2a  8967  lbreu  9017  elfzp12  10220  fihashf1rn  10931  ccatsymb  11056  cau3lem  11396  fsumcl2lem  11680  dvdsnegb  12090  dvds2add  12107  dvds2sub  12108  ndvdssub  12212  gcd2n0cl  12261  divgcdcoprmex  12395  cncongr1  12396  ctinfom  12770  qusecsub  13638  istopfin  14443  toponcom  14470  cnptoprest  14682  dvmptfsum  15168  elply2  15178