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

Theorem anim12i 550
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 20 . 2  |-  ( ( ps  /\  th )  ->  ( ps  /\  th ) )
41, 2, 3syl2an 464 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anim12ci  551  anim1i  552  anim2i  553  sbimi  1664  2mo  2359  cgsex2g  2988  cgsex4g  2989  spc2egv  3038  sseq2  3370  uneqin  3592  undif3  3602  prsspwgOLD  3956  ssunieq  4048  iuneq1  4106  iuneq2  4109  copsex2t  4443  soeq2  4523  tz7.7  4607  eldifpw  4755  iunpw  4759  opbrop  4955  xpsspw  4986  xpsspwOLD  4987  coeq1  5030  coeq2  5031  cnveq  5046  dmeq  5070  sotri  5261  funun  5495  funtp  5503  2elresin  5556  funssxp  5604  fssres  5610  f1co  5648  foun  5693  resdif  5696  f1oco  5698  fvun  5793  fvreseq  5833  dff3  5882  exfo  5887  fprg  5915  ftpg  5916  weisoeq2  6077  ndmovdistr  6236  ndmovord  6237  f1o2ndf1  6454  brrpssg  6524  smores  6614  tfrlem2  6637  tz7.49  6702  tz7.49c  6703  abianfp  6716  oaord  6790  oeeulem  6844  nnaord  6862  brecop  6997  brecop2  6998  eroveu  6999  ecopovtrn  7007  th3qlem1  7010  th3q  7013  ixpeq2  7076  undifixp  7098  undom  7196  sbthlem8  7224  sbthlem9  7225  unxpdom  7316  isinf  7322  f1opwfi  7410  fiin  7427  en2lp  7571  inf3lem3  7585  tcmin  7680  alephfp  7989  kmlem16  8045  cdaval  8050  cdaun  8052  cofsmo  8149  fin23lem28  8220  axdc3lem2  8331  ac6c4  8361  brdom3  8406  brdom5  8407  brdom4  8408  canthp1lem2  8528  finngch  8530  ordpipq  8819  adderpq  8833  mulerpq  8834  lterpq  8847  genpn0  8880  genpnnp  8882  addclprlem2  8894  addcmpblnr  8947  mulcmpblnr  8949  addclsr  8958  addasssr  8963  distrsr  8966  0idsr  8972  1idsr  8973  00sr  8974  mulgt0sr  8980  axaddf  9020  axaddass  9031  axdistr  9033  cnegex  9247  recextlem2  9653  ledivmulOLD  9884  ledivmul2OLD  9888  zaddcl  10317  qaddcl  10590  qmulcl  10592  qreccl  10594  xmulgt0  10862  xrsupsslem  10885  xrinfmsslem  10886  supxrpnf  10897  iccss  10978  difreicc  11028  fzsubel  11088  elfznelfzo  11192  mulexp  11419  mulexpz  11420  leexp1a  11438  faclbnd  11581  hashunx  11660  wrdeq  11738  f1oun2prg  11864  sqabsadd  12087  sqabssub  12088  abs2dif  12136  rexanuz  12149  o1of2  12406  o1rlimmul  12412  fsum2dlem  12554  isumltss  12628  xpnnenOLD  12809  dvdscmulr  12878  dvdsmulcr  12879  dvds2ln  12880  divalglem9  12921  gcdcllem3  13013  gcdaddmlem  13028  gcdabs  13033  sqgcd  13058  qredeq  13106  divgcdodd  13119  pythagtriplem19  13207  xpsfrnel2  13790  isfunc  14061  fpwipodrs  14590  tsrss  14655  resmhm2  14760  gimco  15055  efgrelexlema  15381  gsum2d  15546  dvdsr  15751  subrgpropd  15902  islmhm2  16114  ressmpladd  16520  ressmplmul  16521  mplind  16562  tgcl  17034  uncld  17105  innei  17189  cnco  17330  uncmp  17466  txbas  17599  txbasval  17638  tx1stc  17682  fbun  17872  infil  17895  fbunfip  17901  filuni  17917  imaelfm  17983  txflf  18038  tsmsfbas  18157  tsmsxp  18184  blin2  18459  nmhmplusg  18791  qtopbaslem  18792  iccntr  18852  unmbl  19432  volfiniun  19441  mbfi1flimlem  19614  ply1idom  20047  logreclem  20660  dvdsflip  20967  fsumvma2  20998  chpchtsum  21003  dchrelbas3  21022  dchrmulcl  21033  lgsquad2lem2  21143  dchrisum0fmul  21200  dchrisum0lem1  21210  usgraidx2v  21412  nb3gra2nb  21464  sizeusglecusg  21495  redwlk  21606  wlkdvspthlem  21607  constr3lem6  21636  constr3trllem2  21638  cusconngra  21663  iseupa  21687  gxmul  21866  nvelbl  22185  blocni  22306  hvsub4  22539  shscli  22819  shscom  22821  spanunsni  23081  spanpr  23082  5oalem2  23157  5oalem3  23158  5oalem5  23160  3oalem1  23164  hoscl  23248  hoadddi  23306  hoadddir  23307  hosub4  23316  lnophsi  23504  hmops  23523  hmopm  23524  adjadd  23596  leop2  23627  leopadd  23635  leopmuli  23636  pjclem4  23702  pj3si  23710  mdslmd1lem2  23829  mdslmd3i  23835  atomli  23885  atcvatlem  23888  chirredlem3  23895  chirredi  23897  atcvat3i  23899  mdsymlem1  23906  mdsymlem5  23910  cdjreui  23935  cdj3i  23944  addltmulALT  23949  mndpluscn  24312  sxbrsigalem5  24638  probfinmeasbOLD  24686  txpcon  24919  cvmlift2lem10  24999  ghomgrpilem2  25097  lediv2aALT  25117  fprodser  25275  fprodeq0  25299  fprod2dlem  25304  poseq  25528  wfrlem5  25542  frrlem5  25586  sltres  25619  nocvxminlem  25645  altopeq12  25807  altxpsspw  25822  brcgr  25839  brbtwn2  25844  axcontlem2  25904  funtransport  25965  lukshef-ax2  26165  arg-ax  26166  nndivsub  26207  mblfinlem1  26243  ismblfin  26247  itg2addnclem  26256  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  neibastop1  26388  filnetlem3  26409  fzadd2  26445  prdstotbnd  26503  heibor1lem  26518  isdrngo2  26574  divrngidl  26638  pridlc3  26683  rmxynorm  26981  monotoddzzfi  27005  acongtr  27043  mpaaeu  27332  psgnghm  27414  hashgcdlem  27493  pm10.14  27531  2reu4a  27943  2reu4  27944  oprabv  28085  2elfz2melfz  28117  fz0addge0  28120  2ffzeq  28121  fzonmapblen  28134  2ffzoeq  28140  modifeq2int  28161  2wrdeq  28175  swrdnd  28182  swdeq  28196  swrdswrdlem  28198  swrdccatin12lem3a  28208  swrdccatin2  28210  swrdccatin12lem3  28212  swrdccatin12  28214  swrdccat  28216  cshwidx  28242  2cshw1lem1  28248  2cshw2lem1  28252  cshwleneq  28268  cshweqdif2  28270  cshw1  28275  cshwssizelem1a  28279  2wlkeq  28303  usgra2wlkspthlem1  28306  usgra2pth  28311  usgra2adedgwlkon  28317  el2wlkonotot0  28339  usg2spthonot0  28356  usgrauvtxvd  28363  frgra3v  28392  1to3vfriswmgra  28397  4cycl2v2nb  28406  frgranbnb  28410  frgrawopreg  28438  frg2woteqm  28448  2spotiundisj  28451  frghash2spot  28452  usg2spot2nb  28454  bnj545  29266  bnj546  29267  bnj557  29272  bnj570  29276  bnj594  29283  bnj1001  29329  bnj1118  29353  ax7w9AUX7  29660  linepsubN  30549  pmapsub  30565  elpaddri  30599  paddasslem14  30630  pmapjoin  30649  dvhfvadd  31889  dvhvaddcomN  31894
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