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  5550  f1ocnv  5587  fv3  5652  relelfvdm  5661  funimass4  5686  fvelimab  5692  funconstss  5755  dff2  5781  dffo5  5786  dff1o6  5906  oprabid  6039  ssoprab2i  6099  uchoice  6289  releldm2  6337  ixpf  6875  recexgt0sr  7971  map2psrprg  8003  lediv2a  9053  lbreu  9103  elfzp12  10307  fihashf1rn  11022  ccatsymb  11150  swrdpfx  11254  pfxpfx  11255  pfxccatin12  11280  cau3lem  11640  fsumcl2lem  11924  dvdsnegb  12334  dvds2add  12351  dvds2sub  12352  ndvdssub  12456  gcd2n0cl  12505  divgcdcoprmex  12639  cncongr1  12640  ctinfom  13014  qusecsub  13883  istopfin  14689  toponcom  14716  cnptoprest  14928  dvmptfsum  15414  elply2  15424  uspgr2wlkeqi  16108