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  1652  2mo  2287  cgsex2g  2896  cgsex4g  2897  spc2egv  2946  sseq2  3276  uneqin  3496  undif3  3505  prsspwg  3851  prsspwgOLD  3852  ssunieq  3941  iuneq1  3999  iuneq2  4002  copsex2t  4335  soeq2  4416  tz7.7  4500  eldifpw  4648  iunpw  4652  opbrop  4849  xpsspw  4879  xpsspwOLD  4880  coeq1  4923  coeq2  4924  cnveq  4937  dmeq  4961  sotri  5152  funun  5378  funtp  5385  2elresin  5437  funssxp  5485  fssres  5491  f1co  5529  foun  5574  resdif  5577  f1oco  5579  fvun  5672  fvreseq  5711  dff3  5756  exfo  5761  fprg  5788  weisoeq2  5941  ndmovdistr  6096  ndmovord  6097  brrpssg  6366  smores  6456  tfrlem2  6479  tz7.49  6544  tz7.49c  6545  abianfp  6558  oaord  6632  oeeulem  6686  nnaord  6704  brecop  6839  brecop2  6840  eroveu  6841  ecopovtrn  6849  th3qlem1  6852  th3q  6855  ixpeq2  6918  undifixp  6940  undom  7038  sbthlem8  7066  sbthlem9  7067  unxpdom  7158  isinf  7164  f1opwfi  7249  fiin  7265  en2lp  7407  inf3lem3  7421  tcmin  7516  alephfp  7825  kmlem16  7881  cdaval  7886  cdaun  7888  cofsmo  7985  fin23lem28  8056  axdc3lem2  8167  ac6c4  8198  brdom3  8243  brdom5  8244  brdom4  8245  canthp1lem2  8365  finngch  8367  ordpipq  8656  adderpq  8670  mulerpq  8671  lterpq  8684  genpn0  8717  genpnnp  8719  addclprlem2  8731  addcmpblnr  8784  mulcmpblnr  8786  addclsr  8795  addasssr  8800  distrsr  8803  0idsr  8809  1idsr  8810  00sr  8811  mulgt0sr  8817  axaddf  8857  axaddass  8868  axdistr  8870  cnegex  9083  recextlem2  9489  ledivmulOLD  9720  ledivmul2OLD  9724  zaddcl  10151  qaddcl  10424  qmulcl  10426  qreccl  10428  xmulgt0  10695  xrsupsslem  10717  xrinfmsslem  10718  supxrpnf  10729  iccss  10810  difreicc  10859  fzsubel  10919  mulexp  11234  mulexpz  11235  leexp1a  11253  faclbnd  11396  wrdeq  11520  sqabsadd  11863  sqabssub  11864  abs2dif  11912  rexanuz  11925  o1of2  12182  o1rlimmul  12188  fsum2dlem  12330  isumltss  12404  xpnnenOLD  12585  dvdscmulr  12654  dvdsmulcr  12655  dvds2ln  12656  divalglem9  12697  gcdcllem3  12789  gcdaddmlem  12804  gcdabs  12809  sqgcd  12834  qredeq  12882  divgcdodd  12895  pythagtriplem19  12983  xpsfrnel2  13566  isfunc  13837  fpwipodrs  14366  tsrss  14431  resmhm2  14536  gimco  14831  efgrelexlema  15157  gsum2d  15322  dvdsr  15527  subrgpropd  15678  islmhm2  15894  ressmpladd  16300  ressmplmul  16301  mplind  16342  tgcl  16813  uncld  16884  innei  16968  cnco  17101  uncmp  17236  txbas  17368  txbasval  17407  tx1stc  17450  fbun  17637  infil  17660  fbunfip  17666  filuni  17682  imaelfm  17748  txflf  17803  tsmsfbas  17912  tsmsxp  17939  blin2  18077  nmhmplusg  18368  qtopbaslem  18369  iccntr  18429  unmbl  18999  volfiniun  19008  mbfi1flimlem  19181  ply1idom  19614  logreclem  20227  dvdsflip  20534  fsumvma2  20565  chpchtsum  20570  dchrelbas3  20589  dchrmulcl  20600  lgsquad2lem2  20710  dchrisum0fmul  20767  dchrisum0lem1  20777  gxmul  21057  nvelbl  21376  blocni  21497  hvsub4  21730  shscli  22010  shscom  22012  spanunsni  22272  spanpr  22273  5oalem2  22348  5oalem3  22349  5oalem5  22351  3oalem1  22355  hoscl  22439  hoadddi  22497  hoadddir  22498  hosub4  22507  lnophsi  22695  hmops  22714  hmopm  22715  adjadd  22787  leop2  22818  leopadd  22826  leopmuli  22827  pjclem4  22893  pj3si  22901  mdslmd1lem2  23020  mdslmd3i  23026  atomli  23076  atcvatlem  23079  chirredlem3  23086  chirredi  23088  atcvat3i  23090  mdsymlem1  23097  mdsymlem5  23101  cdjreui  23126  cdj3i  23135  addltmulALT  23140  mndpluscn  23468  insiga  23786  sxval  23810  br2base  23883  sxbrsigalem2  23900  sxbrsigalem5  23902  sxbrsiga  23904  probfinmeasbOLD  23935  ballotlemfc0  23999  ballotlemfcc  24000  txpcon  24167  cvmlift2lem10  24247  iseupa  24285  ghomgrpilem2  24397  lediv2aALT  24417  prodmo  24563  fprodser  24576  fprodeq0  24600  poseq  24811  wfrlem5  24818  frrlem5  24843  sltres  24876  nocvxminlem  24902  altopeq12  25055  altxpsspw  25070  brcgr  25087  brbtwn2  25092  axcontlem2  25152  funtransport  25213  lukshef-ax2  25413  arg-ax  25414  nndivsub  25455  itg2addnclem  25492  itg2addnc  25494  neibastop1  25632  filnetlem3  25653  fzadd2  25768  prdstotbnd  25841  heibor1lem  25856  isdrngo2  25912  divrngidl  25976  pridlc3  26021  rmxynorm  26326  monotoddzzfi  26350  acongtr  26388  mpaaeu  26678  psgnghm  26760  hashgcdlem  26839  pm10.14  26877  2reu4a  27290  2reu4  27291  ftpg  27417  f1oun2prg  27424  elfznelfzo  27462  hashunx  27487  usgraidx2v  27566  nb3gra2nb  27618  sizeusglecusg  27649  redwlk  27742  wlkdvspthlem  27743  constr3lem6  27773  constr3trllem2  27775  cusconngra  27800  frgra3v  27835  1to3vfriswmgra  27840  4cycl2v2nb  27849  frgranbnb  27853  frgrawopreg  27882  bnj545  28689  bnj546  28690  bnj557  28695  bnj570  28699  bnj594  28706  bnj1001  28752  bnj1118  28776  ax7w9AUX7  29077  linepsubN  30010  pmapsub  30026  elpaddri  30060  paddasslem14  30091  pmapjoin  30110  dvhfvadd  31350  dvhvaddcomN  31355
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