MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anim12i 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  1660  2mo  2340  cgsex2g  2956  cgsex4g  2957  spc2egv  3006  sseq2  3338  uneqin  3560  undif3  3570  prsspwgOLD  3924  ssunieq  4016  iuneq1  4074  iuneq2  4077  copsex2t  4411  soeq2  4491  tz7.7  4575  eldifpw  4722  iunpw  4726  opbrop  4922  xpsspw  4953  xpsspwOLD  4954  coeq1  4997  coeq2  4998  cnveq  5013  dmeq  5037  sotri  5228  funun  5462  funtp  5470  2elresin  5523  funssxp  5571  fssres  5577  f1co  5615  foun  5660  resdif  5663  f1oco  5665  fvun  5760  fvreseq  5800  dff3  5849  exfo  5854  fprg  5882  ftpg  5883  weisoeq2  6044  ndmovdistr  6203  ndmovord  6204  f1o2ndf1  6421  brrpssg  6491  smores  6581  tfrlem2  6604  tz7.49  6669  tz7.49c  6670  abianfp  6683  oaord  6757  oeeulem  6811  nnaord  6829  brecop  6964  brecop2  6965  eroveu  6966  ecopovtrn  6974  th3qlem1  6977  th3q  6980  ixpeq2  7043  undifixp  7065  undom  7163  sbthlem8  7191  sbthlem9  7192  unxpdom  7283  isinf  7289  f1opwfi  7376  fiin  7393  en2lp  7535  inf3lem3  7549  tcmin  7644  alephfp  7953  kmlem16  8009  cdaval  8014  cdaun  8016  cofsmo  8113  fin23lem28  8184  axdc3lem2  8295  ac6c4  8325  brdom3  8370  brdom5  8371  brdom4  8372  canthp1lem2  8492  finngch  8494  ordpipq  8783  adderpq  8797  mulerpq  8798  lterpq  8811  genpn0  8844  genpnnp  8846  addclprlem2  8858  addcmpblnr  8911  mulcmpblnr  8913  addclsr  8922  addasssr  8927  distrsr  8930  0idsr  8936  1idsr  8937  00sr  8938  mulgt0sr  8944  axaddf  8984  axaddass  8995  axdistr  8997  cnegex  9211  recextlem2  9617  ledivmulOLD  9848  ledivmul2OLD  9852  zaddcl  10281  qaddcl  10554  qmulcl  10556  qreccl  10558  xmulgt0  10826  xrsupsslem  10849  xrinfmsslem  10850  supxrpnf  10861  iccss  10942  difreicc  10992  fzsubel  11052  elfznelfzo  11155  mulexp  11382  mulexpz  11383  leexp1a  11401  faclbnd  11544  hashunx  11623  wrdeq  11701  f1oun2prg  11827  sqabsadd  12050  sqabssub  12051  abs2dif  12099  rexanuz  12112  o1of2  12369  o1rlimmul  12375  fsum2dlem  12517  isumltss  12591  xpnnenOLD  12772  dvdscmulr  12841  dvdsmulcr  12842  dvds2ln  12843  divalglem9  12884  gcdcllem3  12976  gcdaddmlem  12991  gcdabs  12996  sqgcd  13021  qredeq  13069  divgcdodd  13082  pythagtriplem19  13170  xpsfrnel2  13753  isfunc  14024  fpwipodrs  14553  tsrss  14618  resmhm2  14723  gimco  15018  efgrelexlema  15344  gsum2d  15509  dvdsr  15714  subrgpropd  15865  islmhm2  16077  ressmpladd  16483  ressmplmul  16484  mplind  16525  tgcl  16997  uncld  17068  innei  17152  cnco  17292  uncmp  17428  txbas  17560  txbasval  17599  tx1stc  17643  fbun  17833  infil  17856  fbunfip  17862  filuni  17878  imaelfm  17944  txflf  17999  tsmsfbas  18118  tsmsxp  18145  blin2  18420  nmhmplusg  18752  qtopbaslem  18753  iccntr  18813  unmbl  19393  volfiniun  19402  mbfi1flimlem  19575  ply1idom  20008  logreclem  20621  dvdsflip  20928  fsumvma2  20959  chpchtsum  20964  dchrelbas3  20983  dchrmulcl  20994  lgsquad2lem2  21104  dchrisum0fmul  21161  dchrisum0lem1  21171  usgraidx2v  21373  nb3gra2nb  21425  sizeusglecusg  21456  redwlk  21567  wlkdvspthlem  21568  constr3lem6  21597  constr3trllem2  21599  cusconngra  21624  iseupa  21648  gxmul  21827  nvelbl  22146  blocni  22267  hvsub4  22500  shscli  22780  shscom  22782  spanunsni  23042  spanpr  23043  5oalem2  23118  5oalem3  23119  5oalem5  23121  3oalem1  23125  hoscl  23209  hoadddi  23267  hoadddir  23268  hosub4  23277  lnophsi  23465  hmops  23484  hmopm  23485  adjadd  23557  leop2  23588  leopadd  23596  leopmuli  23597  pjclem4  23663  pj3si  23671  mdslmd1lem2  23790  mdslmd3i  23796  atomli  23846  atcvatlem  23849  chirredlem3  23856  chirredi  23858  atcvat3i  23860  mdsymlem1  23867  mdsymlem5  23871  cdjreui  23896  cdj3i  23905  addltmulALT  23910  mndpluscn  24273  sxbrsigalem5  24599  probfinmeasbOLD  24647  txpcon  24880  cvmlift2lem10  24960  ghomgrpilem2  25058  lediv2aALT  25078  fprodser  25236  fprodeq0  25260  fprod2dlem  25265  poseq  25475  wfrlem5  25482  frrlem5  25507  sltres  25540  nocvxminlem  25566  altopeq12  25719  altxpsspw  25734  brcgr  25751  brbtwn2  25756  axcontlem2  25816  funtransport  25877  lukshef-ax2  26077  arg-ax  26078  nndivsub  26119  mblfinlem  26151  ismblfin  26154  itg2addnclem  26163  neibastop1  26286  filnetlem3  26307  fzadd2  26343  prdstotbnd  26401  heibor1lem  26416  isdrngo2  26472  divrngidl  26536  pridlc3  26581  rmxynorm  26879  monotoddzzfi  26903  acongtr  26941  mpaaeu  27231  psgnghm  27313  hashgcdlem  27392  pm10.14  27430  2reu4a  27842  2reu4  27843  swrdnd  28009  swrdswrdlem  28018  swrdccatin2  28026  swrdccatin12lem3b  28030  swrdccatin12lem3  28032  swrdccatin12  28034  usgra2wlkspthlem1  28044  usgra2pth  28049  usgra2adedgwlkon  28055  el2wlkonotot0  28077  usg2spthonot0  28094  frgra3v  28114  1to3vfriswmgra  28119  4cycl2v2nb  28128  frgranbnb  28132  frgrawopreg  28160  frg2woteqm  28170  2spotiundisj  28173  frghash2spot  28174  usg2spot2nb  28176  bnj545  28984  bnj546  28985  bnj557  28990  bnj570  28994  bnj594  29001  bnj1001  29047  bnj1118  29071  ax7w9AUX7  29372  linepsubN  30246  pmapsub  30262  elpaddri  30296  paddasslem14  30327  pmapjoin  30346  dvhfvadd  31586  dvhvaddcomN  31591
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