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  2253  ordelinel  4491  fun11uni  5318  fabexg  5422  fores  5460  f1oabexg  5484  fun11iun  5493  ssimaex  5584  dffv2  5592  exfo  5678  ndmovass  6008  soxp  6228  tz7.48lem  6453  tz7.49c  6458  omass  6578  oewordri  6590  omabs  6645  sbthlem9  6979  fineqvlem  7077  pssnn  7081  domunfican  7129  fiint  7133  inf1  7323  infeq5  7338  rankuni  7535  acndom  7678  acnnum  7679  cdainflem  7817  cfcof  7900  ac6num  8106  ac6s2  8113  brdom5  8154  brdom4  8155  genpnnp  8629  lediv2a  9650  supmul1  9719  nn2ge  9771  btwnz  10114  eluz2b2  10290  uz2mulcl  10295  eqreznegel  10303  xrsupexmnf  10623  xrinfmexpnf  10624  xrsupsslem  10625  xrinfmsslem  10626  supxrun  10634  ioo0  10681  elioo4g  10711  quoremnn0  10960  modabs  10997  expcl2lem  11115  mulre  11606  rediv  11616  imdiv  11623  resqrex  11736  caurcvg2  12150  tanval  12408  negdvdsb  12545  muldvds1  12553  muldvds2  12554  dvdscmulr  12557  dvdsmulcr  12558  divalglem8  12599  maxprmfct  12792  pcpremul  12896  pcmul  12904  irredn0  15485  lsppratlem1  15900  dvdsrz  16440  clscld  16784  2ndcdisj2  17183  tx1stc  17344  opnfbas  17537  fbasfip  17563  alexsublem  17738  alexsubALTlem4  17744  bcthlem5  18750  vitalilem4  18966  vitalilem5  18967  itg2mulc  19102  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq3  19112  itg2addlem  19113  itg2gt0  19115  itg2cnlem2  19117  dvcobr  19295  dvcnvlem  19323  dvferm1  19332  dvne0  19358  mdegmullem  19464  plyeq0lem  19592  plyexmo  19693  aalioulem5  19716  aalioulem6  19717  aaliou  19718  cxple2a  20046  cxpaddlelem  20091  cxpaddle  20092  bcmono  20516  lgsquadlem2  20594  ex-natded9.20-2  20805  grpoidinvlem3  20873  grpoidinv  20875  ablomul  21022  isdivrngo  21098  sspival  21314  nmobndseqi  21357  nmobndseqiOLD  21358  hvaddsub4  21657  hhcmpl  21779  ocsh  21862  5oalem2  22234  5oalem5  22237  3oalem2  22242  pjjsi  22279  hoadddir  22384  leopmul  22714  stge1i  22818  hatomistici  22942  mdsymlem2  22984  mdsymlem5  22987  addltmulALT  23026  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsup  23063  isoun  23242  xrge0iifhom  23319  sigaclci  23493  cvmsi  23796  elno2  24308  nobndlem6  24351  colinearalg  24538  axcontlem3  24594  trisegint  24651  funtransport  24654  btwnconn1lem4  24713  btwnconn2  24725  segcon2  24728  outsideofeu  24754  lukshef-ax2  24854  limsucncmpi  24884  areacirc  24931  divclrvd  25695  icccon2  25700  isrocatset  25957  fnckleb  26046  isfne  26268  comppfsc  26307  opelopab3  26373  blhalfOLD  26472  isdrngo2  26589  fldcrng  26629  flddmn  26683  cmpfiiin  26772  pellexlem4  26917  pellqrex  26964  acongtr  27065  acongrep  27067  jm2.23  27089  pm10.55  27564  climexp  27731  climsuse  27734  stoweidlem26  27775  stoweidlem35  27784  afvelrn  28030  s4f1o  28093  usgraexmpl  28133  1to3vfriswmgra  28185  bnj529  28770  bnj945  28805  bnj1098  28815  bnj1533  28884  bnj605  28939  bnj594  28944  bnj607  28948  bnj966  28976  bnj967  28977  bnj996  28987  bnj999  28989  bnj1006  28991  bnj1118  29014  bnj1172  29031  bnj1279  29048  bnj1296  29051  bnj1498  29091  cmtbr4N  29445  linepsubN  29941  pmapsub  29957  paddasslem14  30022  pclcmpatN  30090  trlval2  30352  cdleme20  30513  cdleme21j  30525  dvalveclem  31215  dia2dimlem7  31260  dvhlveclem  31298  docaclN  31314  dihjat1  31619  mapdhcl  31917  mapdh6dN  31929  mapdh8  31979  hdmap1l6d  32004  hdmap10  32033  hdmaprnlem17N  32056  hdmaplkr  32106  hdmapip0  32108  hgmapvv  32119
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