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

Theorem pm3.2i 452
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 445 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 9 1  |-  ( ph  /\ 
ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  pm4.87  579  dfbi  622  mp4an  666  3pm3.2i  1159  unssi  3519  ssini  3561  bm1.3ii  4404  epelg  4620  elvv  4884  funpr  5457  mpt2v  6169  caovcom  6249  1st2val  6591  2nd2val  6592  elxp7  6598  tfr1a  6839  oeoa  7024  oeoe  7026  erov  7185  th3q  7197  endisj  7386  phplem2  7479  snopfsupp  7631  cantnffvalOLD  7859  r1funlim  7961  dfac2  8288  cflecard  8410  canth4  8802  canthnumlem  8803  canthwelem  8805  canthp1lem2  8808  pwfseqlem4  8817  wunex3  8896  recexsrlem  9258  mulcani  9963  div1  10011  recdiv  10025  divdiv1  10030  divdiv2  10031  div23i  10077  div11i  10078  divmuldivi  10079  divadddivi  10081  divdivdivi  10082  lemulge11  10179  negiso  10294  dfnn3  10324  2cnne0  10524  2rene0  10525  halfpm6th  10534  avglt1  10550  avglt2  10551  x2times  11250  xrsupsslem  11257  xrinfmsslem  11258  injresinjlem  11622  om2uzoi  11762  fzennn  11774  expge1  11885  faclbnd2  12051  faclbnd4lem1  12053  hashf  12094  hashsnlei  12154  hashunlei  12159  hashsslei  12160  hash2prd  12165  lsw0g  12252  repswccat  12407  cshwsexa  12442  f1oun2prg  12511  wrdlen2i  12530  cjreb  12596  sqr2gt1lt2  12748  abs1m  12807  amgm2  12841  climcndslem2  13296  efcllem  13346  ege2le3  13358  efi4p  13404  efival  13419  sin01bnd  13452  cos01bnd  13453  cos1bnd  13454  cos2bnd  13455  cos01gt0  13458  sin02gt0  13459  sincos2sgn  13461  sin4lt0  13462  egt2lt3  13471  rpnnen2lem3  13482  rpnnen2lem11  13490  nthruc  13516  nthruz  13517  divalglem5  13584  ndvdsi  13597  bitsp1o  13612  pcrec  13908  prmrec  13966  modsubi  14084  structfn  14170  strlemor0  14247  strlemor1  14248  strleun  14251  sscres  14719  ga0  15796  symg2bas  15883  f1otrspeq  15933  0frgp  16256  psrbag0  17508  psrbagsn  17509  coe1mul2  17621  cnfld1  17685  cnsubdrglem  17708  expmhm  17724  expghm  17765  expghmOLD  17766  matmulr  18155  m2detleib  18279  smadiadetglem1  18319  isbasis3g  18396  fctop  18450  cctop  18452  bl2in  19817  dscmet  20007  iihalf1  20345  iihalf2  20347  icopnfhmeo  20357  iccpnfhmeo  20359  xrhmeo  20360  minveclem2  20755  minveclem4  20761  ovolunlem1a  20821  volf  20854  i1f1lem  21009  mbfi1fseqlem5  21039  dveflem  21293  pilem2  21802  pilem3  21803  sinhalfpilem  21810  sincosq1lem  21844  tangtx  21852  sinq12gt0  21854  sincos4thpi  21860  sincos6thpi  21862  sincos3rdpi  21863  pige3  21864  coseq1  21869  efeq1  21870  efif1olem4  21886  angneg  22084  ang180lem1  22090  1cubrlem  22121  quart1  22136  log2cnv  22224  log2tlbnd  22225  log2ublem1  22226  log2ub  22229  emcllem1  22274  emcllem6  22279  basellem1  22303  basellem2  22304  basellem3  22305  basellem8  22310  ppiublem1  22426  ppiublem2  22427  ppiub  22428  chtublem  22435  chtub  22436  bcmono  22501  bclbnd  22504  bpos1lem  22506  bposlem1  22508  bposlem2  22509  bposlem3  22510  bposlem4  22511  bposlem5  22512  bposlem6  22513  bposlem7  22514  bposlem8  22515  bposlem9  22516  lgsdir2lem1  22547  chebbnd1lem1  22603  chebbnd1lem3  22605  chebbnd1  22606  dchrisum0flblem2  22643  dchrisum0lem1  22650  mulog2sumlem2  22669  selberglem2  22680  chpdifbndlem1  22687  ercgrg  22850  axlowdimlem4  23014  axlowdimlem5  23015  axlowdimlem6  23016  axlowdimlem7  23017  axlowdimlem8  23018  axlowdimlem10  23020  axlowdimlem11  23021  usgraexvlem  23136  usgraexmpldifpr  23141  0trl  23268  2trllemH  23274  2trllemE  23275  2wlklemA  23276  2wlklemB  23277  2wlklemC  23278  wlkntrllem2  23282  wlkntrl  23284  0pth  23292  0pthonv  23303  constr1trl  23310  1pthon  23313  1pthon2v  23315  constr2spth  23322  constr2pth  23323  2pthon  23324  2pthon3v  23326  constr3lem1  23354  constr3lem4  23356  constr3trllem3  23361  constr3pthlem2  23365  ex-natded5.2i  23436  ex-an  23452  ex-id  23464  ex-po  23465  ex-fl  23477  cnrngo  23713  nvz0  23879  ipidsq  23931  ipdirilem  24052  siilem1  24074  minvecolem2  24099  minvecolem3  24100  minvecolem4  24104  hvsubcan  24299  hvsubcan2  24300  normlem7tALT  24344  helch  24469  hsn0elch  24474  hhshsslem2  24492  hhsssh  24493  shscli  24543  shintcli  24555  shintcl  24556  chintcli  24557  chintcl  24558  shincli  24588  shsval2i  24613  omlsi  24630  chincli  24686  chabs1  24742  fh1i  24847  fh2i  24848  cm2ji  24851  pjnormi  24947  nmopsetn0  25092  nmfnsetn0  25105  lnophm  25246  nmcexi  25253  nmbdfnlb  25277  imaelshi  25285  nlelshi  25287  nmopadjlem  25316  nmopcoadji  25328  hmopidmch  25380  hmopidmpj  25381  sto1i  25463  stlei  25467  stji1i  25469  csmdsymi  25561  chirred  25622  cdj3lem1  25661  xrsclat  25964  reofld  26162  nn0archi  26165  xrge0iifmhm  26223  cnzh  26253  rezh  26254  qqh0  26267  qqh1  26268  rerrext  26292  cnrrext  26293  prsiga  26428  coinfliprv  26713  ballotlem1  26717  ballotth  26768  signsw0g  26805  signswmnd  26806  subfacval2  26923  erdszelem2  26928  cvmliftlem4  27025  problem4  27149  4bc2eq6  27238  dfpo2  27412  br6  27414  dfon2lem3  27445  poseq  27561  wfrlem13  27583  wfr3  27589  fullfunfnv  27824  bpoly3  28048  onpsstopbas  28124  sin2h  28266  cos2h  28267  tan2h  28268  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  dvtanlem  28285  itg2addnclem2  28288  asindmre  28323  fneref  28400  refref  28401  filnetlem2  28444  filnetlem3  28445  heiborlem7  28560  riscer  28638  ac6s6f  28830  mzpclall  28908  diophin  28956  diophun  28957  eldioph4b  28995  irrapx1  29014  2nn0ind  29131  aomclem4  29255  lhe4.4ex1a  29448  expgrowth  29454  fnchoice  29596  itgsinexplem1  29640  stoweidlem13  29654  stoweidlem14  29655  stoweidlem26  29667  stoweidlem34  29675  stoweidlem49  29690  stoweidlem59  29700  astbstanbst  29769  aistbistaandb  29770  abnotataxb  29777  mdandyv0  29786  mdandyv1  29787  mdandyv2  29788  mdandyv3  29789  mdandyv4  29790  mdandyv5  29791  mdandyv6  29792  mdandyv7  29793  mdandyv8  29794  mdandyv9  29795  mdandyv10  29796  mdandyv11  29797  mdandyv12  29798  mdandyv13  29799  mdandyv14  29800  mdandyv15  29801  mdandyvr0  29802  mdandyvr1  29803  mdandyvr2  29804  mdandyvr3  29805  mdandyvr4  29806  mdandyvr5  29807  mdandyvr6  29808  mdandyvr7  29809  mdandyvrx0  29818  mdandyvrx1  29819  mdandyvrx2  29820  mdandyvrx3  29821  mdandyvrx4  29822  mdandyvrx5  29823  mdandyvrx6  29824  mdandyvrx7  29825  dandysum2p2e4  29835  hash2prv  30072  wlkcomp  30132  usgra2pthspth  30141  usgra2wlkspthlem1  30142  usgra2wlkspthlem2  30143  usgra2pthlem1  30146  usgra2adedgspth  30151  usgra2adedgwlk  30152  usgra2adedgwlkon  30153  usg2wlk  30155  usg2wlkon  30156  el2wlkonot  30234  el2spthonot  30235  el2spthonot0  30236  usg2wlkonot  30248  usg2wotspth  30249  clwlkcomp  30272  frgrancvvdgeq  30482  numclwwlk1  30537  numclwwlk2lem3  30545  frgraregord013  30557  zlmodzxzlmod  30585  zlmodzxzel  30586  zlmodzxzscm  30588  zlmodzxzadd  30589  psgnsn  30602  snlindsntorlem  30713  ldepspr  30716  lmod1lem2  30739  lmod1lem3  30740  lmod1lem4  30741  lmod1lem5  30742  lmodn0  30746  zlmodzxznm  30748  zlmodzxzldeplem  30749  zlmodzxzldeplem1  30751  zlmodzxzldeplem3  30753  lvecpsslmod  30758  ldepsnlinc  30759  ldepslinc  30760  dpfrac1  30816  alimp-surprise  30839  ax6e2nd  30968  uun0.1  31213  relopabVD  31339  ax6e2ndVD  31346  sb5ALTVD  31351  ax6e2ndALT  31368  bj-2upln1upl  32100  ishlatiN  32573  0psubN  32966  atpsubN  32970  taupilem1  35188
  Copyright terms: Public domain W3C validator