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

Theorem anim1i 551
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 19 . 2  |-  ( ch 
->  ch )
31, 2anim12i 549 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sylanl1  631  sylanr1  633  disamis  2266  ordelinel  4507  fun11uni  5334  fabexg  5438  fores  5476  f1oabexg  5500  fun11iun  5509  ssimaex  5600  dffv2  5608  exfo  5694  ndmovass  6024  soxp  6244  tz7.48lem  6469  tz7.49c  6474  omass  6594  oewordri  6606  omabs  6661  sbthlem9  6995  fineqvlem  7093  pssnn  7097  domunfican  7145  fiint  7149  inf1  7339  infeq5  7354  rankuni  7551  acndom  7694  acnnum  7695  cdainflem  7833  cfcof  7916  ac6num  8122  ac6s2  8129  brdom5  8170  brdom4  8171  genpnnp  8645  lediv2a  9666  supmul1  9735  nn2ge  9787  btwnz  10130  eluz2b2  10306  uz2mulcl  10311  eqreznegel  10319  xrsupexmnf  10639  xrinfmexpnf  10640  xrsupsslem  10641  xrinfmsslem  10642  supxrun  10650  ioo0  10697  elioo4g  10727  quoremnn0  10976  modabs  11013  expcl2lem  11131  mulre  11622  rediv  11632  imdiv  11639  resqrex  11752  caurcvg2  12166  tanval  12424  negdvdsb  12561  muldvds1  12569  muldvds2  12570  dvdscmulr  12573  dvdsmulcr  12574  divalglem8  12615  maxprmfct  12808  pcpremul  12912  pcmul  12920  irredn0  15501  lsppratlem1  15916  dvdsrz  16456  clscld  16800  2ndcdisj2  17199  tx1stc  17360  opnfbas  17553  fbasfip  17579  alexsublem  17754  alexsubALTlem4  17760  bcthlem5  18766  vitalilem4  18982  vitalilem5  18983  itg2mulc  19118  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq3  19128  itg2addlem  19129  itg2gt0  19131  itg2cnlem2  19133  dvcobr  19311  dvcnvlem  19339  dvferm1  19348  dvne0  19374  mdegmullem  19480  plyeq0lem  19608  plyexmo  19709  aalioulem5  19732  aalioulem6  19733  aaliou  19734  cxple2a  20062  cxpaddlelem  20107  cxpaddle  20108  bcmono  20532  lgsquadlem2  20610  ex-natded9.20-2  20821  grpoidinvlem3  20889  grpoidinv  20891  ablomul  21038  isdivrngo  21114  sspival  21330  nmobndseqi  21373  nmobndseqiOLD  21374  hvaddsub4  21673  hhcmpl  21795  ocsh  21878  5oalem2  22250  5oalem5  22253  3oalem2  22258  pjjsi  22295  hoadddir  22400  leopmul  22730  stge1i  22834  hatomistici  22958  mdsymlem2  23000  mdsymlem5  23003  addltmulALT  23042  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemsup  23079  isoun  23257  xrge0iifhom  23334  sigaclci  23508  cvmsi  23811  elno2  24379  nobndlem6  24422  colinearalg  24610  axcontlem3  24666  trisegint  24723  funtransport  24726  btwnconn1lem4  24785  btwnconn2  24797  segcon2  24800  outsideofeu  24826  lukshef-ax2  24926  limsucncmpi  24956  itg2gt0cn  25006  bddiblnc  25021  areacirc  25034  divclrvd  25798  icccon2  25803  isrocatset  26060  fnckleb  26149  isfne  26371  comppfsc  26410  opelopab3  26476  blhalfOLD  26575  isdrngo2  26692  fldcrng  26732  flddmn  26786  cmpfiiin  26875  pellexlem4  27020  pellqrex  27067  acongtr  27168  acongrep  27170  jm2.23  27192  pm10.55  27667  climexp  27834  climsuse  27837  stoweidlem26  27878  stoweidlem35  27887  afvelrn  28136  s4f1o  28225  usgraexmpl  28267  nb3grapr  28289  nb3grapr2  28290  nb3gra2nb  28291  fargshiftfva  28384  eupatrl  28385  1to3vfriswmgra  28431  bnj529  29086  bnj945  29121  bnj1098  29131  bnj1533  29200  bnj605  29255  bnj594  29260  bnj607  29264  bnj966  29292  bnj967  29293  bnj996  29303  bnj999  29305  bnj1006  29307  bnj1118  29330  bnj1172  29347  bnj1279  29364  bnj1296  29367  bnj1498  29407  cmtbr4N  30067  linepsubN  30563  pmapsub  30579  paddasslem14  30644  pclcmpatN  30712  trlval2  30974  cdleme20  31135  cdleme21j  31147  dvalveclem  31837  dia2dimlem7  31882  dvhlveclem  31920  docaclN  31936  dihjat1  32241  mapdhcl  32539  mapdh6dN  32551  mapdh8  32601  hdmap1l6d  32626  hdmap10  32655  hdmaprnlem17N  32678  hdmaplkr  32728  hdmapip0  32730  hgmapvv  32741
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 177  df-an 360
  Copyright terms: Public domain W3C validator