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  823  xoranor  1419  19.41h  1731  sbimi  1810  equs5e  1841  exdistrfor  1846  equs45f  1848  sbidm  1897  eu3h  2123  eupickb  2159  2exeu  2170  darii  2178  festino  2184  baroco  2185  r19.27v  2658  r19.27av  2666  rspc2ev  2922  reu3  2993  difdif  3329  ssddif  3438  inssdif  3440  difin  3441  difindiss  3458  indifdir  3460  difrab  3478  iundif2ss  4031  trssord  4471  ordsuc  4655  find  4691  imainss  5144  dffun5r  5330  fof  5548  f1ocnv  5585  fv3  5650  relelfvdm  5659  funimass4  5684  fvelimab  5690  funconstss  5753  dff2  5779  dffo5  5784  dff1o6  5900  oprabid  6033  ssoprab2i  6093  uchoice  6283  releldm2  6331  ixpf  6867  recexgt0sr  7960  map2psrprg  7992  lediv2a  9042  lbreu  9092  elfzp12  10295  fihashf1rn  11010  ccatsymb  11137  swrdpfx  11239  pfxpfx  11240  pfxccatin12  11265  cau3lem  11625  fsumcl2lem  11909  dvdsnegb  12319  dvds2add  12336  dvds2sub  12337  ndvdssub  12441  gcd2n0cl  12490  divgcdcoprmex  12624  cncongr1  12625  ctinfom  12999  qusecsub  13868  istopfin  14674  toponcom  14701  cnptoprest  14913  dvmptfsum  15399  elply2  15409  uspgr2wlkeqi  16078