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

Theorem anim12i 551
Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
Hypotheses
Ref Expression
anim12i.1  |-  ( ph  ->  ps )
anim12i.2  |-  ( ch 
->  th )
Assertion
Ref Expression
anim12i  |-  ( (
ph  /\  ch )  ->  ( ps  /\  th ) )

Proof of Theorem anim12i
StepHypRef Expression
1 anim12i.1 . 2  |-  ( ph  ->  ps )
2 anim12i.2 . 2  |-  ( ch 
->  th )
3 id 21 . 2  |-  ( ( ps  /\  th )  ->  ( ps  /\  th ) )
41, 2, 3syl2an 465 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  anim12ci  552  anim1i  553  anim2i  554  sbimi  1665  2mo  2361  cgsex2g  2990  cgsex4g  2991  spc2egv  3040  sseq2  3372  uneqin  3594  undif3  3604  prsspwgOLD  3958  ssunieq  4050  iuneq1  4108  iuneq2  4111  copsex2t  4446  soeq2  4526  tz7.7  4610  eldifpw  4758  iunpw  4762  opbrop  4958  xpsspw  4989  xpsspwOLD  4990  coeq1  5033  coeq2  5034  cnveq  5049  dmeq  5073  sotri  5264  funun  5498  funtp  5506  2elresin  5559  funssxp  5607  fssres  5613  f1co  5651  foun  5696  resdif  5699  f1oco  5701  fvun  5796  fvreseq  5836  dff3  5885  exfo  5890  fprg  5918  ftpg  5919  weisoeq2  6080  ndmovdistr  6239  ndmovord  6240  f1o2ndf1  6457  brrpssg  6527  smores  6617  tfrlem2  6640  tz7.49  6705  tz7.49c  6706  abianfp  6719  oaord  6793  oeeulem  6847  nnaord  6865  brecop  7000  brecop2  7001  eroveu  7002  ecopovtrn  7010  th3qlem1  7013  th3q  7016  ixpeq2  7079  undifixp  7101  undom  7199  sbthlem8  7227  sbthlem9  7228  unxpdom  7319  isinf  7325  f1opwfi  7413  fiin  7430  en2lp  7574  inf3lem3  7588  tcmin  7683  alephfp  7994  kmlem16  8050  cdaval  8055  cdaun  8057  cofsmo  8154  fin23lem28  8225  axdc3lem2  8336  ac6c4  8366  brdom3  8411  brdom5  8412  brdom4  8413  canthp1lem2  8533  finngch  8535  ordpipq  8824  adderpq  8838  mulerpq  8839  lterpq  8852  genpn0  8885  genpnnp  8887  addclprlem2  8899  addcmpblnr  8952  mulcmpblnr  8954  addclsr  8963  addasssr  8968  distrsr  8971  0idsr  8977  1idsr  8978  00sr  8979  mulgt0sr  8985  axaddf  9025  axaddass  9036  axdistr  9038  cnegex  9252  recextlem2  9658  ledivmulOLD  9889  ledivmul2OLD  9893  zaddcl  10322  qaddcl  10595  qmulcl  10597  qreccl  10599  xmulgt0  10867  xrsupsslem  10890  xrinfmsslem  10891  supxrpnf  10902  iccss  10983  difreicc  11033  fzsubel  11093  elfznelfzo  11197  mulexp  11424  mulexpz  11425  leexp1a  11443  faclbnd  11586  hashunx  11665  wrdeq  11743  f1oun2prg  11869  sqabsadd  12092  sqabssub  12093  abs2dif  12141  rexanuz  12154  o1of2  12411  o1rlimmul  12417  fsum2dlem  12559  isumltss  12633  xpnnenOLD  12814  dvdscmulr  12883  dvdsmulcr  12884  dvds2ln  12885  divalglem9  12926  gcdcllem3  13018  gcdaddmlem  13033  gcdabs  13038  sqgcd  13063  qredeq  13111  divgcdodd  13124  pythagtriplem19  13212  xpsfrnel2  13795  isfunc  14066  fpwipodrs  14595  tsrss  14660  resmhm2  14765  gimco  15060  efgrelexlema  15386  gsum2d  15551  dvdsr  15756  subrgpropd  15907  islmhm2  16119  ressmpladd  16525  ressmplmul  16526  mplind  16567  tgcl  17039  uncld  17110  innei  17194  cnco  17335  uncmp  17471  txbas  17604  txbasval  17643  tx1stc  17687  fbun  17877  infil  17900  fbunfip  17906  filuni  17922  imaelfm  17988  txflf  18043  tsmsfbas  18162  tsmsxp  18189  blin2  18464  nmhmplusg  18796  qtopbaslem  18797  iccntr  18857  unmbl  19437  volfiniun  19446  mbfi1flimlem  19617  ply1idom  20052  logreclem  20665  dvdsflip  20972  fsumvma2  21003  chpchtsum  21008  dchrelbas3  21027  dchrmulcl  21038  lgsquad2lem2  21148  dchrisum0fmul  21205  dchrisum0lem1  21215  usgraidx2v  21417  nb3gra2nb  21469  sizeusglecusg  21500  redwlk  21611  wlkdvspthlem  21612  constr3lem6  21641  constr3trllem2  21643  cusconngra  21668  iseupa  21692  gxmul  21871  nvelbl  22190  blocni  22311  hvsub4  22544  shscli  22824  shscom  22826  spanunsni  23086  spanpr  23087  5oalem2  23162  5oalem3  23163  5oalem5  23165  3oalem1  23169  hoscl  23253  hoadddi  23311  hoadddir  23312  hosub4  23321  lnophsi  23509  hmops  23528  hmopm  23529  adjadd  23601  leop2  23632  leopadd  23640  leopmuli  23641  pjclem4  23707  pj3si  23715  mdslmd1lem2  23834  mdslmd3i  23840  atomli  23890  atcvatlem  23893  chirredlem3  23900  chirredi  23902  atcvat3i  23904  mdsymlem1  23911  mdsymlem5  23915  cdjreui  23940  cdj3i  23949  addltmulALT  23954  mndpluscn  24317  sxbrsigalem5  24643  probfinmeasbOLD  24691  txpcon  24924  cvmlift2lem10  25004  ghomgrpilem2  25102  lediv2aALT  25122  fprodser  25280  fprodeq0  25304  fprod2dlem  25309  poseq  25533  wfrlem5  25547  frrlem5  25591  sltres  25624  nocvxminlem  25650  altopeq12  25812  altxpsspw  25827  brcgr  25844  brbtwn2  25849  axcontlem2  25909  funtransport  25970  lukshef-ax2  26170  arg-ax  26171  nndivsub  26212  heicant  26253  mblfinlem1  26255  ismblfin  26259  itg2addnclem  26270  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  neibastop1  26402  filnetlem3  26423  fzadd2  26459  prdstotbnd  26517  heibor1lem  26532  isdrngo2  26588  divrngidl  26652  pridlc3  26697  rmxynorm  26995  monotoddzzfi  27019  acongtr  27057  mpaaeu  27346  psgnghm  27428  hashgcdlem  27507  pm10.14  27545  2reu4a  27957  2reu4  27958  oprabv  28103  elovmpt3rab1  28107  2elfz2melfz  28140  fz0addge0  28143  2ffzeq  28144  fzonmapblen  28157  2ffzoeq  28163  modifeq2int  28184  2wrdeq  28207  swrdnd  28216  swdeq  28230  swrdswrdlem  28232  swrdccatin12lem3a  28242  swrdccatin2  28244  swrdccatin12lem3  28246  swrdccatin12  28248  swrdccat  28250  cshwidx  28276  2cshw1lem1  28282  2cshw2lem1  28286  cshwleneq  28302  cshweqdif2  28304  cshw1  28309  cshwssizelem1a  28313  2wlkeq  28341  usgra2wlkspthlem1  28344  usgra2pth  28349  usgra2adedgwlkon  28355  el2wlkonotot0  28404  usg2spthonot0  28421  usgrauvtxvd  28428  frgra3v  28466  1to3vfriswmgra  28471  4cycl2v2nb  28480  frgranbnb  28484  frgrawopreg  28512  frg2woteqm  28522  2spotiundisj  28525  frghash2spot  28526  usg2spot2nb  28528  bnj545  29340  bnj546  29341  bnj557  29346  bnj570  29350  bnj594  29357  bnj1001  29403  bnj1118  29427  ax7w9AUX7  29734  linepsubN  30623  pmapsub  30639  elpaddri  30673  paddasslem14  30704  pmapjoin  30723  dvhfvadd  31963  dvhvaddcomN  31968
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 179  df-an 362
  Copyright terms: Public domain W3C validator