MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim2i Structured version   Unicode version

Theorem anim2i 553
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
StepHypRef Expression
1 id 20 . 2  |-  ( ch 
->  ch )
2 anim1i.1 . 2  |-  ( ph  ->  ps )
31, 2anim12i 550 1  |-  ( ( ch  /\  ph )  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sylanl2  633  sylanr2  635  andi  838  sbimi  1664  19.41OLD  1901  exdistrf  2062  exdistrfOLD  2063  equs45f  2084  eupickb  2345  2eu1  2360  darii  2379  festino  2385  baroco  2386  r19.27av  2836  rspc2ev  3052  reu3  3116  difrab  3607  trssord  4590  ordnbtwn  4664  tfi  4825  find  4862  imainss  5279  fof  5645  f1ocnv  5679  fv3  5736  fvelimab  5774  dff2  5873  dffo5  5878  dff1o6  6005  oprabid  6097  ssoprab2i  6154  ndmovass  6227  ndmovdistr  6228  releldm2  6389  bropopvvv  6418  tfrlem5  6633  omlimcl  6813  odi  6814  ixpf  7076  infcntss  7372  hartogs  7505  card2on  7514  epfrs  7659  acni3  7920  dfac2  8003  cflm  8122  axdc2lem  8320  ac6s  8356  ondomon  8430  axregndlem1  8469  axregnd  8471  eltsk2g  8618  grothpw  8693  grothpwex  8694  grothomex  8696  ltexprlem1  8905  ltexprlem4  8908  recexsrlem  8970  lediv2a  9896  lbreu  9950  elfzp12  11118  cau3lem  12150  rlimres  12344  dvdsnegb  12859  dvds2add  12873  dvds2sub  12874  ndvdssub  12919  isfunc  14053  drsdirfi  14387  spweu  14651  gimcnv  15046  gaid  15068  lmhmlem  16097  lmimcnv  16131  abvn0b  16354  prmirredlem  16765  toponcom  16987  neitr  17236  cnprest  17345  nrmsep2  17412  2ndcsep  17514  reghaus  17849  isfil2  17880  alexsubALTlem3  18072  cnextcn  18090  lpbl  18525  iscau4  19224  caussi  19242  cmetcuspOLD  19299  cmetcusp  19300  ovolicc2lem3  19407  limcresi  19764  elply2  20107  elqaa  20231  aannenlem1  20237  aannenlem2  20238  bpos1lem  21058  uhgrares  21335  usgrares  21381  usgraexmpl  21412  cusgra3v  21465  cusgrafilem2  21481  redwlk  21598  wlkdvspthlem  21599  cyclispthon  21612  usgrcyclnl1  21619  3v3e3cycl1  21623  eupatrl  21682  isgrpo  21776  gxsub  21856  rngmgmbs4  21997  vcz  22041  sspival  22229  hvsub4  22531  hvaddsub4  22572  5oalem2  23149  5oalem5  23152  5oalem6  23153  3oalem2  23157  homcl  23241  hoadddi  23298  stle0i  23734  spansncv2  23788  mdsymlem1  23898  cdj3lem1  23929  disjin  24019  sxbrsigalem0  24613  dya2icoseg2  24620  ballotlemirc  24781  axcont  25907  colineardim1  25987  idinside  26010  lukshef-ax2  26157  ovoliunnfl  26238  itg2addnclem  26246  finminlem  26312  ivthALT  26329  indexa  26426  sstotbnd3  26476  heibor1lem  26509  heibor1  26510  eldioph4i  26864  acongtr  27034  aaitgo  27335  dvsconst  27515  stoweidlem17  27733  dmfcoafv  28006  f13dfv  28067  swrdccatin2  28176  swrdccatin12lem3  28178  swrdccatin12  28180  cshwidx  28208  cshwidxm1  28211  cshwidxm  28212  cshwidxn  28213  2cshw2lem1  28218  cshwssizelem2  28244  cshwssizelem4a  28246  2wlkonotv  28297  frgraunss  28322  frgranbnb  28347  frgrawopreg  28375  frg2woteq  28386  bnj145  29031  bnj168  29034  bnj546  29204  bnj594  29220  bnj1097  29287  bnj1110  29288  bnj1174  29309  bnj1176  29311  ax12olem2wAUX7  29393  exdistrfNEW7  29442  equs45fNEW7  29558  ax12olem2OLD7  29643  dalem53  30459  dalem54  30460  linepsubN  30486  pmapsub  30502  elpaddri  30536  pclfinN  30634  pclcmpatN  30635  cdlemg33c0  31436  dihatexv2  32074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator