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

Theorem anim12i 566
Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
Hypotheses
Ref Expression
anim12i.1
anim12i.2
Assertion
Ref Expression
anim12i

Proof of Theorem anim12i
StepHypRef Expression
1 anim12i.1 . 2
2 anim12i.2 . 2
3 id 22 . 2
41, 2, 3syl2an 477 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  anim12ci  567  anim1i  568  anim2i  569  sbimi  1745  2moOLD  2374  cgsex2g  3143  cgsex4g  3144  spc2egv  3196  sseq2  3525  uneqin  3748  undif3  3758  ssunieq  4284  iuneq1  4344  iuneq2  4347  copsex2t  4739  soeq2  4825  tz7.7  4909  opbrop  5084  xpsspw  5121  xpsspwOLD  5122  coeq1  5165  coeq2  5166  cnveq  5181  dmeq  5208  sotri  5399  funun  5635  fununfun  5637  funtp  5645  2elresin  5697  funssxp  5749  fssres  5756  f1co  5795  foun  5839  resdif  5841  f1oco  5843  fvun  5943  elfvmptrab1  5976  fvn0ssdmfun  6022  dff3  6044  exfo  6049  fprg  6080  ftpg  6081  weisoeq2  6252  oprabv  6345  ndmovdistr  6464  ndmovord  6465  brrpssg  6582  eldifpw  6612  iunpw  6614  f1o2ndf1  6908  fvn0elsupp  6934  fvn0elsuppOLD  6935  smores  7042  tz7.49  7129  tz7.49c  7130  oaord  7215  oeeulem  7269  nnaord  7287  brecop  7423  brecop2  7424  eroveu  7425  ecopovtrn  7433  ixpeq2  7503  undifixp  7525  undom  7625  sbthlem8  7654  sbthlem9  7655  unxpdom  7747  isinf  7753  f1opwfi  7844  fiin  7902  en2lp  8051  inf3lem3  8068  tcmin  8193  alephfp  8510  kmlem16  8566  cdaval  8571  cdaun  8573  cofsmo  8670  fin23lem28  8741  axdc3lem2  8852  ac6c4  8882  brdom3  8927  brdom5  8928  brdom4  8929  canthp1lem2  9052  finngch  9054  ordpipq  9341  adderpq  9355  mulerpq  9356  lterpq  9369  genpn0  9402  genpnnp  9404  addclprlem2  9416  addcmpblnr  9467  addsrpr  9473  mulsrpr  9474  addclsr  9481  addasssr  9486  distrsr  9489  0idsr  9495  1idsr  9496  00sr  9497  mulgt0sr  9503  axaddf  9543  axaddass  9554  axdistr  9556  cnegex  9782  recextlem2  10205  ledivmulOLD  10444  ledivmul2OLD  10448  zaddcl  10929  qaddcl  11227  qmulcl  11229  qreccl  11231  xmulgt0  11504  xrsupsslem  11527  xrinfmsslem  11528  supxrpnf  11539  iccss  11621  difreicc  11681  fzsubel  11748  elfz0add  11804  difelfznle  11818  2ffzeq  11823  fzonmapblen  11868  ubmelfzo  11881  ubmelm1fzo  11908  elfznelfzo  11915  addmodid  12036  modifeq2int  12049  modaddmodup  12050  fsuppmapnn0fiub  12097  mulexp  12205  mulexpz  12206  leexp1a  12224  faclbnd  12368  hashunx  12454  wrdeq  12564  swrdnd  12657  swrdeq  12671  swrdsymbeq  12672  swrdswrdlem  12684  reuccats1  12706  swrdccatin12lem2a  12710  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12  12716  swrdccat  12718  repswswrd  12756  repswccat  12757  cshwidxn  12779  cshweqdif2  12787  2cshwcshw  12793  cshwcshid  12795  cshwcsh2id  12796  f1oun2prg  12865  s2eq2s1eq  12881  wwlktovf1  12895  sqabsadd  13115  sqabssub  13116  abs2dif  13165  rexanuz  13178  o1of2  13435  o1rlimmul  13441  fsum2dlem  13585  isumltss  13660  fprodser  13756  fprodeq0  13779  fprod2dlem  13784  xpnnenOLD  13943  dvdscmulr  14012  dvdsmulcr  14013  dvds2ln  14014  divalglem9  14059  gcdcllem3  14151  gcdaddmlem  14166  gcdabs  14171  sqgcd  14196  qredeq  14247  divgcdodd  14260  pythagtriplem19  14357  cshwsidrepsw  14578  xpsfrnel2  14962  isfunc  15233  fpwipodrs  15794  tsrss  15853  resmhm2  15991  gimco  16316  symg2bas  16423  pgrpsubgsymg  16433  symgextf  16442  gsmsymgrfixlem1  16452  fvcosymgeq  16454  gsmsymgreqlem1  16455  symgfixf1  16462  efgrelexlema  16767  gsum2dlem1  16997  gsum2dlem2  16998  gsum2dOLD  17000  dvdsr  17295  subrgpropd  17463  islmhm2  17684  ressmpladd  18119  ressmplmul  18120  mplind  18167  psgnghm  18616  psgndiflemB  18636  frlmbas3  18807  frlmphl  18812  islindf4  18873  mpt2matmul  18948  mavmul0g  19055  1marepvsma1  19085  mdetdiag  19101  slesolvec  19181  cramerimplem2  19186  cramerimplem3  19187  cramerimp  19188  mat2pmatlin  19236  m2pmfzgsumcl  19249  monmatcollpw  19280  pmatcollpw3lem  19284  pmatcollpwscmatlem1  19290  chpmat1dlem  19336  chfacfisf  19355  chfacfisfcpmat  19356  chfacfpmmulgsum2  19366  tgcl  19471  uncld  19542  innei  19626  cnco  19767  uncmp  19903  txbas  20068  txbasval  20107  tx1stc  20151  fbun  20341  infil  20364  fbunfip  20370  filuni  20386  imaelfm  20452  txflf  20507  tsmsfbas  20626  tsmsxp  20657  blin2  20932  nmhmplusg  21264  qtopbaslem  21265  iccntr  21326  unmbl  21948  volfiniun  21957  mbfi1flimlem  22129  ply1idom  22525  logreclem  23150  dvdsflip  23458  fsumvma2  23489  chpchtsum  23494  dchrelbas3  23513  dchrmulcl  23524  lgsquad2lem2  23634  dchrisum0fmul  23691  dchrisum0lem1  23701  ishpg  24128  brcgr  24203  brbtwn2  24208  axcontlem2  24268  usgraidx2v  24393  nb3gra2nb  24455  sizeusglecusg  24486  redwlk  24608  wlkdvspthlem  24609  usgra2adedgwlkon  24615  usgra2wlkspthlem1  24619  constr3lem6  24649  constr3trllem2  24651  cusconngra  24676  2wlkeq  24707  usg2wlkeq2  24709  wwlkextinj  24730  clwlkisclwwlklem2a  24785  clwlkisclwwlklem0  24788  clwwisshclww  24807  clwlkf1clwwlk  24850  el2wlkonotot0  24872  usg2spthonot0  24889  rusgranumwlkl1  24947  rusgra0edg  24955  iseupa  24965  frgra3v  25002  1to3vfriswmgra  25007  4cycl2v2nb  25016  frgranbnb  25020  frgrawopreg  25049  frg2woteqm  25059  2spotiundisj  25062  frghash2spot  25063  usg2spot2nb  25065  extwwlkfablem2  25078  numclwwlkovgelim  25089  numclwlk1lem2fo  25095  numclwwlk2  25107  frgrareggt1  25116  gxmul  25280  nvelbl  25599  blocni  25720  hvsub4  25954  shscli  26235  shscom  26237  spanunsni  26497  spanpr  26498  5oalem2  26573  5oalem3  26574  5oalem5  26576  3oalem1  26580  hoscl  26664  hoadddi  26722  hoadddir  26723  hosub4  26732  lnophsi  26920  hmops  26939  hmopm  26940  adjadd  27012  leop2  27043  leopadd  27051  leopmuli  27052  pjclem4  27118  pj3si  27126  mdslmd1lem2  27245  mdslmd3i  27251  atomli  27301  atcvatlem  27304  chirredlem3  27311  chirredi  27313  atcvat3i  27315  mdsymlem1  27322  mdsymlem5  27326  cdjreui  27351  cdj3i  27360  addltmulALT  27365  spc2ed  27372  mndpluscn  27908  sxbrsigalem5  28259  probfinmeasbOLD  28367  txpcon  28677  cvmlift2lem10  28757  ghomgrpilem2  29026  lediv2aALT  29043  poseq  29333  wfrlem5  29347  frrlem5  29391  sltres  29424  nocvxminlem  29450  altopeq12  29612  altxpsspw  29627  funtransport  29681  lukshef-ax2  29880  arg-ax  29881  nndivsub  29922  wl-ax11-lem2  30026  heicant  30049  mblfinlem1  30051  ismblfin  30055  itg2addnclem  30066  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  neibastop1  30177  filnetlem3  30198  fzadd2  30234  prdstotbnd  30290  heibor1lem  30305  isdrngo2  30361  divrngidl  30425  pridlc3  30470  rmxynorm  30854  monotoddzzfi  30878  acongtr  30916  mpaaeu  31099  hashgcdlem  31157  isprm7  31192  lcmcllem  31202  lcmabs  31211  lcmgcdlem  31212  lcmgcd  31213  lcmgcdeq  31216  nzin  31223  pm10.14  31264  etransclem38  32055  2reu4a  32194  2reu4  32195  2elfz2melfz  32334  fz0addge0  32335  2ffzoeq  32341  usgra2pth  32354  usgrauvtxvd  32358  uhguhgra  32372  usgedgvadf1  32415  usgedgvadf1ALT  32418  rabsubmgmd  32479  resmgmhm2  32487  ismhm0  32493  mhmismgmhm  32494  isrnghmmul  32699  c0ghm  32717  rhmisrnghm  32726  rnghmsubcsetclem2  32784  rngcinv  32789  rngcinvOLD  32801  rhmsubcsetclem2  32830  rhmsubcrngclem2  32836  ringcinv  32840  ringcinvOLD  32864  srhmsubc  32884  srhmsubcOLD  32903  mapprop  32935  zlmodzxzadd  32947  domnmsuppn0  32962  mndpfsupp  32969  ply1mulgsumlem2  32987  lincsum  33030  lincsumcl  33032  lincscmcl  33033  isldepslvec2  33086  bnj545  33953  bnj546  33954  bnj557  33959  bnj570  33963  bnj594  33970  bnj1001  34016  bnj1118  34040  anifp  34158  linepsubN  35476  pmapsub  35492  elpaddri  35526  paddasslem14  35557  pmapjoin  35576  dvhfvadd  36818  dvhvaddcomN  36823  trclubg  37785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator