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  2332  cgsex2g  2948  cgsex4g  2949  spc2egv  2998  sseq2  3330  uneqin  3552  undif3  3562  prsspwgOLD  3916  ssunieq  4008  iuneq1  4066  iuneq2  4069  copsex2t  4403  soeq2  4483  tz7.7  4567  eldifpw  4714  iunpw  4718  opbrop  4914  xpsspw  4945  xpsspwOLD  4946  coeq1  4989  coeq2  4990  cnveq  5005  dmeq  5029  sotri  5220  funun  5454  funtp  5462  2elresin  5515  funssxp  5563  fssres  5569  f1co  5607  foun  5652  resdif  5655  f1oco  5657  fvun  5752  fvreseq  5792  dff3  5841  exfo  5846  fprg  5874  ftpg  5875  weisoeq2  6036  ndmovdistr  6195  ndmovord  6196  f1o2ndf1  6413  brrpssg  6483  smores  6573  tfrlem2  6596  tz7.49  6661  tz7.49c  6662  abianfp  6675  oaord  6749  oeeulem  6803  nnaord  6821  brecop  6956  brecop2  6957  eroveu  6958  ecopovtrn  6966  th3qlem1  6969  th3q  6972  ixpeq2  7035  undifixp  7057  undom  7155  sbthlem8  7183  sbthlem9  7184  unxpdom  7275  isinf  7281  f1opwfi  7368  fiin  7385  en2lp  7527  inf3lem3  7541  tcmin  7636  alephfp  7945  kmlem16  8001  cdaval  8006  cdaun  8008  cofsmo  8105  fin23lem28  8176  axdc3lem2  8287  ac6c4  8317  brdom3  8362  brdom5  8363  brdom4  8364  canthp1lem2  8484  finngch  8486  ordpipq  8775  adderpq  8789  mulerpq  8790  lterpq  8803  genpn0  8836  genpnnp  8838  addclprlem2  8850  addcmpblnr  8903  mulcmpblnr  8905  addclsr  8914  addasssr  8919  distrsr  8922  0idsr  8928  1idsr  8929  00sr  8930  mulgt0sr  8936  axaddf  8976  axaddass  8987  axdistr  8989  cnegex  9203  recextlem2  9609  ledivmulOLD  9840  ledivmul2OLD  9844  zaddcl  10273  qaddcl  10546  qmulcl  10548  qreccl  10550  xmulgt0  10818  xrsupsslem  10841  xrinfmsslem  10842  supxrpnf  10853  iccss  10934  difreicc  10984  fzsubel  11044  elfznelfzo  11147  mulexp  11374  mulexpz  11375  leexp1a  11393  faclbnd  11536  hashunx  11615  wrdeq  11693  f1oun2prg  11819  sqabsadd  12042  sqabssub  12043  abs2dif  12091  rexanuz  12104  o1of2  12361  o1rlimmul  12367  fsum2dlem  12509  isumltss  12583  xpnnenOLD  12764  dvdscmulr  12833  dvdsmulcr  12834  dvds2ln  12835  divalglem9  12876  gcdcllem3  12968  gcdaddmlem  12983  gcdabs  12988  sqgcd  13013  qredeq  13061  divgcdodd  13074  pythagtriplem19  13162  xpsfrnel2  13745  isfunc  14016  fpwipodrs  14545  tsrss  14610  resmhm2  14715  gimco  15010  efgrelexlema  15336  gsum2d  15501  dvdsr  15706  subrgpropd  15857  islmhm2  16069  ressmpladd  16475  ressmplmul  16476  mplind  16517  tgcl  16989  uncld  17060  innei  17144  cnco  17284  uncmp  17420  txbas  17552  txbasval  17591  tx1stc  17635  fbun  17825  infil  17848  fbunfip  17854  filuni  17870  imaelfm  17936  txflf  17991  tsmsfbas  18110  tsmsxp  18137  blin2  18412  nmhmplusg  18744  qtopbaslem  18745  iccntr  18805  unmbl  19385  volfiniun  19394  mbfi1flimlem  19567  ply1idom  20000  logreclem  20613  dvdsflip  20920  fsumvma2  20951  chpchtsum  20956  dchrelbas3  20975  dchrmulcl  20986  lgsquad2lem2  21096  dchrisum0fmul  21153  dchrisum0lem1  21163  usgraidx2v  21365  nb3gra2nb  21417  sizeusglecusg  21448  redwlk  21559  wlkdvspthlem  21560  constr3lem6  21589  constr3trllem2  21591  cusconngra  21616  iseupa  21640  gxmul  21819  nvelbl  22138  blocni  22259  hvsub4  22492  shscli  22772  shscom  22774  spanunsni  23034  spanpr  23035  5oalem2  23110  5oalem3  23111  5oalem5  23113  3oalem1  23117  hoscl  23201  hoadddi  23259  hoadddir  23260  hosub4  23269  lnophsi  23457  hmops  23476  hmopm  23477  adjadd  23549  leop2  23580  leopadd  23588  leopmuli  23589  pjclem4  23655  pj3si  23663  mdslmd1lem2  23782  mdslmd3i  23788  atomli  23838  atcvatlem  23841  chirredlem3  23848  chirredi  23850  atcvat3i  23852  mdsymlem1  23859  mdsymlem5  23863  cdjreui  23888  cdj3i  23897  addltmulALT  23902  mndpluscn  24265  sxbrsigalem5  24591  probfinmeasbOLD  24639  txpcon  24872  cvmlift2lem10  24952  ghomgrpilem2  25050  lediv2aALT  25070  fprodser  25228  fprodeq0  25252  fprod2dlem  25257  poseq  25467  wfrlem5  25474  frrlem5  25499  sltres  25532  nocvxminlem  25558  altopeq12  25711  altxpsspw  25726  brcgr  25743  brbtwn2  25748  axcontlem2  25808  funtransport  25869  lukshef-ax2  26069  arg-ax  26070  nndivsub  26111  mblfinlem  26143  ismblfin  26146  itg2addnclem  26155  neibastop1  26278  filnetlem3  26299  fzadd2  26335  prdstotbnd  26393  heibor1lem  26408  isdrngo2  26464  divrngidl  26528  pridlc3  26573  rmxynorm  26871  monotoddzzfi  26895  acongtr  26933  mpaaeu  27223  psgnghm  27305  hashgcdlem  27384  pm10.14  27422  2reu4a  27834  2reu4  27835  swrdnd  28001  swrdswrdlem  28010  swrdccatin2  28018  swrdccatin12lem3b  28022  swrdccatin12lem3  28024  swrdccatin12  28026  usgra2wlkspthlem1  28036  usgra2pth  28041  usgra2adedgwlkon  28047  el2wlkonotot0  28069  usg2spthonot0  28086  frgra3v  28106  1to3vfriswmgra  28111  4cycl2v2nb  28120  frgranbnb  28124  frgrawopreg  28152  frg2woteqm  28162  2spotiundisj  28165  frghash2spot  28166  usg2spot2nb  28168  bnj545  28972  bnj546  28973  bnj557  28978  bnj570  28982  bnj594  28989  bnj1001  29035  bnj1118  29059  ax7w9AUX7  29360  linepsubN  30234  pmapsub  30250  elpaddri  30284  paddasslem14  30315  pmapjoin  30334  dvhfvadd  31574  dvhvaddcomN  31579
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