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  1388  19.41h  1699  sbimi  1778  equs5e  1809  exdistrfor  1814  equs45f  1816  sbidm  1865  eu3h  2090  eupickb  2126  2exeu  2137  darii  2145  festino  2151  baroco  2152  r19.27v  2624  r19.27av  2632  rspc2ev  2883  reu3  2954  difdif  3289  ssddif  3398  inssdif  3400  difin  3401  difindiss  3418  indifdir  3420  difrab  3438  iundif2ss  3983  trssord  4416  ordsuc  4600  find  4636  imainss  5086  dffun5r  5271  fof  5483  f1ocnv  5520  fv3  5584  relelfvdm  5593  funimass4  5614  fvelimab  5620  funconstss  5683  dff2  5709  dffo5  5714  dff1o6  5826  oprabid  5957  ssoprab2i  6015  uchoice  6204  releldm2  6252  ixpf  6788  recexgt0sr  7857  map2psrprg  7889  lediv2a  8939  lbreu  8989  elfzp12  10191  fihashf1rn  10897  cau3lem  11296  fsumcl2lem  11580  dvdsnegb  11990  dvds2add  12007  dvds2sub  12008  ndvdssub  12112  gcd2n0cl  12161  divgcdcoprmex  12295  cncongr1  12296  ctinfom  12670  qusecsub  13537  istopfin  14320  toponcom  14347  cnptoprest  14559  dvmptfsum  15045  elply2  15055