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  3288  ssddif  3397  inssdif  3399  difin  3400  difindiss  3417  indifdir  3419  difrab  3437  iundif2ss  3982  trssord  4415  ordsuc  4599  find  4635  imainss  5085  dffun5r  5270  fof  5480  f1ocnv  5517  fv3  5581  relelfvdm  5590  funimass4  5611  fvelimab  5617  funconstss  5680  dff2  5706  dffo5  5711  dff1o6  5823  oprabid  5954  ssoprab2i  6011  uchoice  6195  releldm2  6243  ixpf  6779  recexgt0sr  7840  map2psrprg  7872  lediv2a  8922  lbreu  8972  elfzp12  10174  fihashf1rn  10880  cau3lem  11279  fsumcl2lem  11563  dvdsnegb  11973  dvds2add  11990  dvds2sub  11991  ndvdssub  12095  gcd2n0cl  12136  divgcdcoprmex  12270  cncongr1  12271  ctinfom  12645  qusecsub  13461  istopfin  14236  toponcom  14263  cnptoprest  14475  dvmptfsum  14961  elply2  14971