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  818  pm4.55dc  938  xoranor  1377  19.41h  1685  sbimi  1764  equs5e  1795  exdistrfor  1800  equs45f  1802  sbidm  1851  eu3h  2071  eupickb  2107  2exeu  2118  darii  2126  festino  2132  baroco  2133  r19.27v  2604  r19.27av  2612  rspc2ev  2858  reu3  2929  difdif  3262  ssddif  3371  inssdif  3373  difin  3374  difindiss  3391  indifdir  3393  difrab  3411  iundif2ss  3954  trssord  4382  ordsuc  4564  find  4600  imainss  5046  dffun5r  5230  fof  5440  f1ocnv  5476  fv3  5540  relelfvdm  5549  funimass4  5569  fvelimab  5575  funconstss  5637  dff2  5663  dffo5  5668  dff1o6  5780  oprabid  5910  ssoprab2i  5967  releldm2  6189  ixpf  6723  recexgt0sr  7775  map2psrprg  7807  lediv2a  8855  lbreu  8905  elfzp12  10102  fihashf1rn  10771  cau3lem  11126  fsumcl2lem  11409  dvdsnegb  11818  dvds2add  11835  dvds2sub  11836  ndvdssub  11938  gcd2n0cl  11973  divgcdcoprmex  12105  cncongr1  12106  ctinfom  12432  istopfin  13688  toponcom  13715  cnptoprest  13927