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

Theorem pm3.2i 441
Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
pm3.2i.1  |-  ph
pm3.2i.2  |-  ps
Assertion
Ref Expression
pm3.2i  |-  ( ph  /\ 
ps )

Proof of Theorem pm3.2i
StepHypRef Expression
1 pm3.2i.1 . 2  |-  ph
2 pm3.2i.2 . 2  |-  ps
3 pm3.2 434 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 17 1  |-  ( ph  /\ 
ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 358
This theorem is referenced by:  pm4.87  567  dfbi  610  mp4an  654  3pm3.2i  1130  pm11.07  2054  unssi  3350  ssini  3392  bm1.3ii  4144  epelg  4306  elvv  4748  funpr  5302  mpt2v  5937  caovcom  6017  1st2val  6145  2nd2val  6146  elxp7  6152  tfr1a  6410  oeoa  6595  oeoe  6597  erov  6755  th3q  6767  endisj  6949  phplem2  7041  r1funlim  7438  dfac2  7757  cflecard  7879  canth4  8269  canthnumlem  8270  canthwelem  8272  canthp1lem2  8275  pwfseqlem4  8284  wunex3  8363  recexsrlem  8725  mulcani  9407  div1  9453  recdiv  9466  divdiv1  9471  divdiv2  9472  div23i  9518  div11i  9519  divmuldivi  9520  divadddivi  9522  divdivdivi  9523  lemulge11  9618  negiso  9730  dfnn3  9760  1mhlfehlf  9934  halfpm6th  9936  2halves  9940  halfaddsub  9945  avglt1  9949  avglt2  9950  nneo  10095  zeo  10097  x2times  10619  xrsupsslem  10625  xrinfmsslem  10626  om2uzoi  11018  fzennn  11030  expge1  11139  faclbnd2  11304  faclbnd4lem1  11306  hashf  11344  hashsnlei  11376  hashunlei  11377  hashsslei  11378  cjreb  11608  sqr2gt1lt2  11760  abs1m  11819  amgm2  11853  climcndslem2  12309  efcllem  12359  ege2le3  12371  efi4p  12417  efival  12432  cosmul  12453  sin01bnd  12465  cos01bnd  12466  cos1bnd  12467  cos2bnd  12468  cos01gt0  12471  sin02gt0  12472  sincos2sgn  12474  sin4lt0  12475  egt2lt3  12484  rpnnen2lem3  12495  rpnnen2lem11  12503  nthruc  12529  nthruz  12530  odd2np1  12587  divalglem5  12596  ndvdsi  12609  bitsp1o  12624  pythagtriplem12  12879  pythagtriplem14  12881  pythagtriplem15  12882  pythagtriplem16  12883  pythagtriplem17  12884  pcrec  12911  prmrec  12969  modsubi  13087  structfn  13161  strlemor0  13234  strlemor1  13235  strleun  13238  sscres  13700  ga0  14752  0frgp  15088  psrbag0  16235  psrbagsn  16236  cnfld1  16399  cnsubdrglem  16422  expmhm  16449  expghm  16450  isbasis3g  16687  fctop  16741  cctop  16743  bl2in  17957  dscmet  18095  iihalf1  18429  iihalf2  18431  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  minveclem2  18790  minveclem4  18796  ovolunlem1a  18855  volf  18888  i1f1lem  19044  mbfi1fseqlem5  19074  dveflem  19326  pilem2  19828  pilem3  19829  sinhalfpilem  19834  ptolemy  19864  sincosq1lem  19865  sincosq4sgn  19869  tangtx  19873  sinq12gt0  19875  sincos4thpi  19881  sincos6thpi  19883  sincos3rdpi  19884  pige3  19885  coskpi  19888  coseq1  19890  efeq1  19891  efif1olem4  19907  dvsqr  20084  angneg  20101  ang180lem1  20107  ang180lem2  20108  1cubrlem  20137  dquartlem1  20147  quart1  20152  atan1  20224  log2cnv  20240  log2tlbnd  20241  log2ublem1  20242  log2ub  20245  emcllem1  20289  emcllem6  20294  basellem1  20318  basellem2  20319  basellem3  20320  basellem8  20325  ppiublem1  20441  ppiublem2  20442  ppiub  20443  chtublem  20450  chtub  20451  bcmono  20516  bclbnd  20519  bpos1lem  20521  bposlem1  20523  bposlem2  20524  bposlem3  20525  bposlem4  20526  bposlem5  20527  bposlem6  20528  bposlem7  20529  bposlem8  20530  bposlem9  20531  lgsdir2lem1  20562  chebbnd1lem1  20618  chebbnd1lem3  20620  chebbnd1  20621  dchrisum0flblem2  20658  dchrisum0lem1  20665  mulog2sumlem2  20684  selberglem2  20695  chpdifbndlem1  20702  ex-natded5.2i  20793  ex-an  20809  ex-id  20821  ex-po  20822  ex-fl  20834  cnrngo  21070  nvz0  21234  ipidsq  21286  ipdirilem  21407  siilem1  21429  minvecolem2  21454  minvecolem3  21455  minvecolem4  21459  hvsubcan  21653  hvsubcan2  21654  normlem7tALT  21698  helch  21823  hsn0elch  21827  hhshsslem2  21845  hhsssh  21846  shscli  21896  shintcli  21908  shintcl  21909  chintcli  21910  chintcl  21911  shincli  21941  shsval2i  21966  omlsi  21983  chincli  22039  chabs1  22095  fh1i  22200  fh2i  22201  cm2ji  22204  pjnormi  22300  nmopsetn0  22445  nmfnsetn0  22458  lnophm  22599  nmcexi  22606  nmbdfnlb  22630  imaelshi  22638  nlelshi  22640  nmopadjlem  22669  nmopcoadji  22681  hmopidmch  22733  hmopidmpj  22734  sto1i  22816  stlei  22820  stji1i  22822  csmdsymi  22914  chirred  22975  cdj3lem1  23014  rinvf1o  23038  ballotlem1  23045  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemimin  23064  ballotlemsdom  23070  ballotlemsel1i  23071  ballotlemsima  23074  ballotlemfrceq  23087  ballotlemfrcn0  23088  ballotth  23096  tpr2rico  23296  xrge0iifmhm  23321  dmvlsiga  23490  prsiga  23492  measbase  23528  ismeas  23530  coinfliprv  23683  coinflippvt  23685  subfacval2  23718  erdszelem2  23723  cvmliftlem4  23819  4bc2eq6  24099  dfpo2  24112  br6  24114  dfon2lem3  24141  poseq  24253  wfrlem13  24268  wfr3  24275  fullfunfnv  24484  axlowdimlem4  24573  axlowdimlem5  24574  axlowdimlem6  24575  axlowdimlem7  24576  axlowdimlem8  24577  axlowdimlem10  24579  axlowdimlem11  24580  bpoly3  24793  onpsstopbas  24869  imfstnrelc  25081  repcpwti  25161  toplat  25290  intopcoaconb  25540  cntrset  25602  mslb1  25607  msra3  25609  claddrv  25647  sigadd  25649  addassv  25656  issubrv  25672  subclrvd  25674  clsmulcv  25682  clsmulrv  25683  fnmulcv  25684  1ded  25738  0ded  25757  0catOLD  25758  1cat  25759  dualalg  25782  catsbc  25849  cmpidmor3  25970  setiscat  25979  fnckle  26045  pfsubkl  26047  pgapspf  26052  pgapspf2  26053  linevala2  26078  pdiveql  26168  fneref  26284  refref  26285  filnetlem2  26328  filnetlem3  26329  heiborlem6  26540  heiborlem7  26541  riscer  26619  mzpclall  26805  diophin  26852  diophun  26853  ftp  26893  eldioph4b  26894  irrapx1  26913  2nn0ind  27030  aomclem4  27154  f1otrspeq  27390  matmulr  27467  lhe4.4ex1a  27546  expgrowth  27552  fnchoice  27700  infrglb  27722  dvcosre  27741  itgsin0pilem1  27744  itgsinexplem1  27748  itgsinexp  27749  stoweidlem5  27754  stoweidlem7  27756  stoweidlem13  27762  stoweidlem14  27763  stoweidlem24  27773  stoweidlem26  27775  stoweidlem28  27777  stoweidlem34  27783  stoweidlem44  27793  stoweidlem49  27798  stoweidlem59  27808  stoweid  27812  wallispilem2  27815  wallispilem3  27816  wallispilem4  27817  wallispi  27819  wallispi2lem1  27820  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem13  27835  stirlinglem15  27837  bothtbothsame  27867  bothfbothsame  27868  aiffbbtat  27869  aisbbisfaisf  27870  aibnbna  27874  aiffbtbat  27876  astbstanbst  27877  aistbistaandb  27878  abnotbtaxb  27884  abnotataxb  27885  mdandyv0  27894  mdandyv1  27895  mdandyv2  27896  mdandyv3  27897  mdandyv4  27898  mdandyv5  27899  mdandyv6  27900  mdandyv7  27901  mdandyv8  27902  mdandyv9  27903  mdandyv10  27904  mdandyv11  27905  mdandyv12  27906  mdandyv13  27907  mdandyv14  27908  mdandyv15  27909  mdandyvr0  27910  mdandyvr1  27911  mdandyvr2  27912  mdandyvr3  27913  mdandyvr4  27914  mdandyvr5  27915  mdandyvr6  27916  mdandyvr7  27917  mdandyvr8  27918  mdandyvr9  27919  mdandyvr10  27920  mdandyvr11  27921  mdandyvr12  27922  mdandyvr13  27923  mdandyvr14  27924  mdandyvr15  27925  mdandyvrx0  27926  mdandyvrx1  27927  mdandyvrx2  27928  mdandyvrx3  27929  mdandyvrx4  27930  mdandyvrx5  27931  mdandyvrx6  27932  mdandyvrx7  27933  mdandyvrx8  27934  mdandyvrx9  27935  mdandyvrx10  27936  mdandyvrx11  27937  mdandyvrx12  27938  mdandyvrx13  27939  mdandyvrx14  27940  mdandyvrx15  27941  dandysum2p2e4  27943  f1oun2prg  28076  usgraexvlem  28127  usgraexmpldifpr  28132  dpfrac1  28242  a9e2nd  28324  uun0.1  28553  relopabVD  28677  a9e2ndVD  28684  sb5ALTVD  28689  a9e2ndALT  28707  ishlatiN  29545  0psubN  29938  atpsubN  29942
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