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

Theorem anim12i 549
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 19 . 2  |-  ( ( ps  /\  th )  ->  ( ps  /\  th ) )
41, 2, 3syl2an 463 1  |-  ( (
ph  /\  ch )  ->  ( ps  /\  th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anim12ci  550  anim1i  551  anim2i  552  sbimi  1633  2mo  2221  cgsex2g  2820  cgsex4g  2821  spc2egv  2870  sseq2  3200  uneqin  3420  undif3  3429  ssunieq  3860  iuneq1  3918  iuneq2  3921  copsex2t  4253  soeq2  4334  tz7.7  4418  eldifpw  4566  iunpw  4570  opbrop  4767  xpsspw  4797  xpsspwOLD  4798  coeq1  4841  coeq2  4842  cnveq  4855  dmeq  4879  sotri  5070  funun  5296  funtp  5303  2elresin  5355  funssxp  5402  fssres  5408  f1co  5446  foun  5491  resdif  5494  f1oco  5496  fvun  5589  fvreseq  5628  dff3  5673  exfo  5678  weisoeq2  5854  ndmovdistr  6009  ndmovord  6010  brrpssg  6279  smores  6369  tfrlem2  6392  tz7.49  6457  tz7.49c  6458  abianfp  6471  oaord  6545  oeeulem  6599  nnaord  6617  brecop  6751  brecop2  6752  eroveu  6753  ecopovtrn  6761  th3qlem1  6764  th3q  6767  ixpeq2  6830  undifixp  6852  undom  6950  sbthlem8  6978  sbthlem9  6979  unxpdom  7070  isinf  7076  f1opwfi  7159  fiin  7175  en2lp  7317  inf3lem3  7331  tcmin  7426  alephfp  7735  kmlem16  7791  cdaval  7796  cdaun  7798  cofsmo  7895  fin23lem28  7966  axdc3lem2  8077  ac6c4  8108  brdom3  8153  brdom5  8154  brdom4  8155  canthp1lem2  8275  finngch  8277  ordpipq  8566  adderpq  8580  mulerpq  8581  lterpq  8594  genpn0  8627  genpnnp  8629  addclprlem2  8641  addcmpblnr  8694  mulcmpblnr  8696  addclsr  8705  addasssr  8710  distrsr  8713  0idsr  8719  1idsr  8720  00sr  8721  mulgt0sr  8727  axaddf  8767  axaddass  8778  axdistr  8780  cnegex  8993  recextlem2  9399  ledivmulOLD  9630  ledivmul2OLD  9634  zaddcl  10059  qaddcl  10332  qmulcl  10334  qreccl  10336  xmulgt0  10603  xrsupsslem  10625  xrinfmsslem  10626  supxrpnf  10637  iccss  10718  difreicc  10767  fzsubel  10827  mulexp  11141  mulexpz  11142  leexp1a  11160  faclbnd  11303  wrdeq  11424  sqabsadd  11767  sqabssub  11768  abs2dif  11816  rexanuz  11829  o1of2  12086  o1rlimmul  12092  fsum2dlem  12233  isumltss  12307  xpnnenOLD  12488  dvdscmulr  12557  dvdsmulcr  12558  dvds2ln  12559  divalglem9  12600  gcdcllem3  12692  gcdaddmlem  12707  gcdabs  12712  sqgcd  12737  qredeq  12785  divgcdodd  12798  pythagtriplem19  12886  xpsfrnel2  13467  isfunc  13738  fpwipodrs  14267  tsrss  14332  resmhm2  14437  gimco  14732  efgrelexlema  15058  gsum2d  15223  dvdsr  15428  subrgpropd  15579  islmhm2  15795  ressmpladd  16201  ressmplmul  16202  mplind  16243  tgcl  16707  uncld  16778  innei  16862  cnco  16995  uncmp  17130  txbas  17262  txbasval  17301  tx1stc  17344  fbun  17535  infil  17558  fbunfip  17564  filuni  17580  imaelfm  17646  txflf  17701  tsmsfbas  17810  tsmsxp  17837  blin2  17975  nmhmplusg  18266  qtopbaslem  18267  iccntr  18326  unmbl  18895  volfiniun  18904  mbfi1flimlem  19077  ply1idom  19510  logreclem  20116  dvdsflip  20422  fsumvma2  20453  chpchtsum  20458  dchrelbas3  20477  dchrmulcl  20488  lgsquad2lem2  20598  dchrisum0fmul  20655  dchrisum0lem1  20665  gxmul  20945  nvelbl  21262  blocni  21383  hvsub4  21616  shscli  21896  shscom  21898  spanunsni  22158  spanpr  22159  5oalem2  22234  5oalem3  22235  5oalem5  22237  3oalem1  22241  hoscl  22325  hoadddi  22383  hoadddir  22384  hosub4  22393  lnophsi  22581  hmops  22600  hmopm  22601  adjadd  22673  leop2  22704  leopadd  22712  leopmuli  22713  pjclem4  22779  pj3si  22787  mdslmd1lem2  22906  mdslmd3i  22912  atomli  22962  atcvatlem  22965  chirredlem3  22972  chirredi  22974  atcvat3i  22976  mdsymlem1  22983  mdsymlem5  22987  cdjreui  23012  cdj3i  23021  addltmulALT  23026  ballotlemfc0  23051  ballotlemfcc  23052  prsspwg  23184  mndpluscn  23299  insiga  23498  sxval  23521  br2base  23574  probfinmeasbOLD  23631  txpcon  23763  cvmlift2lem10  23843  iseupa  23881  ghomgrpilem2  23993  lediv2aALT  24013  poseq  24253  wfrlem5  24260  frrlem5  24285  sltres  24318  nocvxminlem  24344  altopeq12  24496  altxpsspw  24511  brcgr  24528  brbtwn2  24533  axcontlem2  24593  funtransport  24654  lukshef-ax2  24854  arg-ax  24855  nndivsub  24896  elo  25041  celsor  25111  fprg  25133  ubos  25256  inposet  25278  intopcoaconlem3b  25538  fil2ss  25557  limptlimpr2lem1  25574  mslb1  25607  2wsms  25608  lvsovso  25626  icccon4  25702  ismonc  25814  isepic  25824  fnctartar2  25908  cmp2morpdom  25964  pgapspf2  26053  neibastop1  26308  filnetlem3  26329  fzadd2  26444  prdstotbnd  26518  heibor1lem  26533  isdrngo2  26589  divrngidl  26653  pridlc3  26698  rmxynorm  27003  monotoddzzfi  27027  acongtr  27065  mpaaeu  27355  psgnghm  27437  hashgcdlem  27516  pm10.14  27554  2reu4a  27967  2reu4  27968  f1oun2prg  28076  frgra3v  28180  1to3vfriswmgra  28185  bnj545  28927  bnj546  28928  bnj557  28933  bnj570  28937  bnj594  28944  bnj1001  28990  bnj1118  29014  linepsubN  29941  pmapsub  29957  elpaddri  29991  paddasslem14  30022  pmapjoin  30041  dvhfvadd  31281  dvhvaddcomN  31286
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 177  df-an 360
  Copyright terms: Public domain W3C validator