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

Theorem anim1i 552
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
anim1i  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )

Proof of Theorem anim1i
StepHypRef Expression
1 anim1i.1 . 2  |-  ( ph  ->  ps )
2 id 20 . 2  |-  ( ch 
->  ch )
31, 2anim12i 550 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sylanl1  632  sylanr1  634  disamis  2390  ordelinel  4672  fun11uni  5511  fabexg  5616  fores  5654  f1oabexg  5678  fun11iun  5687  ssimaex  5780  dffv2  5788  exfo  5879  ndmovass  6227  soxp  6451  tz7.48lem  6690  tz7.49c  6695  omass  6815  oewordri  6827  omabs  6882  sbthlem9  7217  fineqvlem  7315  pssnn  7319  domunfican  7371  fiint  7375  inf1  7569  infeq5  7584  rankuni  7781  acndom  7924  acnnum  7925  cdainflem  8063  cfcof  8146  ac6num  8351  ac6s2  8358  brdom5  8399  brdom4  8400  genpnnp  8874  lediv2a  9896  supmul1  9965  nn2ge  10017  btwnz  10364  eluz2b2  10540  uz2mulcl  10545  eqreznegel  10553  xrsupexmnf  10875  xrinfmexpnf  10876  xrsupsslem  10877  xrinfmsslem  10878  supxrun  10886  ioo0  10933  elioo4g  10963  quoremnn0  11229  modabs  11266  expcl2lem  11385  s4f1o  11857  mulre  11918  rediv  11928  imdiv  11935  resqrex  12048  caurcvg2  12463  tanval  12721  negdvdsb  12858  muldvds1  12866  muldvds2  12867  dvdscmulr  12870  dvdsmulcr  12871  divalglem8  12912  maxprmfct  13105  pcpremul  13209  pcmul  13217  irredn0  15800  lsppratlem1  16211  dvdsrz  16759  clscld  17103  neiptopnei  17188  2ndcdisj2  17512  tx1stc  17674  opnfbas  17866  fbasfip  17892  alexsublem  18067  alexsubALTlem4  18073  cnextcn  18090  bcthlem5  19273  vitalilem4  19495  vitalilem5  19496  itg2mulc  19631  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2mono  19637  itg2i1fseqle  19638  itg2i1fseq3  19641  itg2addlem  19642  itg2gt0  19644  itg2cnlem2  19646  dvcobr  19824  dvcnvlem  19852  dvferm1  19861  dvne0  19887  mdegmullem  19993  plyeq0lem  20121  plyexmo  20222  aalioulem5  20245  aalioulem6  20246  aaliou  20247  cxple2a  20582  cxpaddlelem  20627  cxpaddle  20628  bcmono  21053  lgsquadlem2  21131  usgraexmpl  21412  nb3grapr  21454  nb3grapr2  21455  nb3gra2nb  21456  cusgrarn  21460  cusgrasizeindslem3  21476  spthonepeq  21579  fargshiftfva  21618  vdusgraval  21670  eupatrl  21682  ex-natded9.20-2  21718  grpoidinvlem3  21786  grpoidinv  21788  ablomul  21935  isdivrngo  22011  sspival  22229  nmobndseqi  22272  nmobndseqiOLD  22273  hvaddsub4  22572  hhcmpl  22694  ocsh  22777  5oalem2  23149  5oalem5  23152  3oalem2  23157  pjjsi  23194  hoadddir  23299  leopmul  23629  stge1i  23733  hatomistici  23857  mdsymlem2  23899  mdsymlem5  23902  addltmulALT  23941  isoun  24081  qqhre  24378  sxbrsigalem0  24613  dya2iocnei  24624  sxbrsigalem5  24630  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemsup  24754  cvmsi  24944  elno2  25601  nobndlem6  25644  colinearalg  25841  axcontlem3  25897  trisegint  25954  funtransport  25957  btwnconn1lem4  26016  btwnconn2  26028  segcon2  26031  outsideofeu  26057  lukshef-ax2  26157  limsucncmpi  26187  ismblfin  26237  itg2addnc  26249  itg2gt0cn  26250  bddiblnc  26265  ftc1anclem6  26275  ftc1anclem8  26277  ftc1anc  26278  areacirc  26288  isfne  26339  comppfsc  26378  opelopab3  26409  isdrngo2  26565  fldcrng  26605  flddmn  26659  cmpfiiin  26742  pellexlem4  26886  pellqrex  26933  acongtr  27034  acongrep  27036  jm2.23  27058  pm10.55  27532  refsum2cnlem1  27675  fmuldfeq  27680  climsuse  27701  stoweidlem26  27742  stoweidlem52  27768  stoweidlem57  27773  afvelrn  27999  lesubnn0  28081  elfz2z  28089  fz0fzelfz0  28102  fz0fzdiffz0  28103  modaddmulmod  28136  modifeq2int  28139  swrdccatin2  28176  swrdccatin12lem4  28179  swrdccat3  28181  swrdccat3blem  28184  modprm0  28194  cshwidx  28208  2cshw1lem1  28214  2cshw1lem2  28215  cshweqdif2s  28234  cshw1  28238  cshwssizesame  28251  usg2spthonot1  28310  1to3vfriswmgra  28334  frgranbnb  28347  vdfrgra0  28349  vdgfrgra0  28350  vdgn0frgrav2  28352  vdgn1frgrav2  28354  frgrawopreg  28375  frg2wot1  28383  usg2spot2nb  28391  bnj529  29046  bnj945  29081  bnj1098  29091  bnj1533  29160  bnj605  29215  bnj594  29220  bnj607  29224  bnj966  29252  bnj967  29253  bnj996  29263  bnj999  29265  bnj1006  29267  bnj1118  29290  bnj1172  29307  bnj1279  29324  bnj1296  29327  bnj1498  29367  ax7w10AUX7  29599  cmtbr4N  29990  linepsubN  30486  pmapsub  30502  paddasslem14  30567  pclcmpatN  30635  trlval2  30897  cdleme20  31058  cdleme21j  31070  dvalveclem  31760  dia2dimlem7  31805  dvhlveclem  31843  docaclN  31859  dihjat1  32164  mapdhcl  32462  mapdh6dN  32474  mapdh8  32524  hdmap1l6d  32549  hdmap10  32578  hdmaprnlem17N  32601  hdmaplkr  32651  hdmapip0  32653  hgmapvv  32664
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