Theorem anim2i 340

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 336	1 |- ( ( ch /\ ph ) -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylanl2  401  sylanr2  403  andi  813  pm4.55dc  933  xoranor  1372  19.41h  1678  sbimi  1757  equs5e  1788  exdistrfor  1793  equs45f  1795  sbidm  1844  eu3h  2064  eupickb  2100  2exeu  2111  darii  2119  festino  2125  baroco  2126  r19.27v  2597  r19.27av  2605  rspc2ev  2849  reu3  2920  difdif  3252  ssddif  3361  inssdif  3363  difin  3364  difindiss  3381  indifdir  3383  difrab  3401  iundif2ss  3938  trssord  4365  ordsuc  4547  find  4583  imainss  5026  dffun5r  5210  fof  5420  f1ocnv  5455  fv3  5519  relelfvdm  5528  funimass4  5547  fvelimab  5552  funconstss  5614  dff2  5640  dffo5  5645  dff1o6  5755  oprabid  5885  ssoprab2i  5942  releldm2  6164  ixpf  6698  recexgt0sr  7735  map2psrprg  7767  lediv2a  8811  lbreu  8861  elfzp12  10055  focdmex  10721  fihashf1rn  10723  cau3lem  11078  fsumcl2lem  11361  dvdsnegb  11770  dvds2add  11787  dvds2sub  11788  ndvdssub  11889  gcd2n0cl  11924  divgcdcoprmex  12056  cncongr1  12057  ctinfom  12383  istopfin  12792  toponcom  12819  cnptoprest  13033