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

Theorem pm3.2i 461
Description: Infer conjunction of premises. (Contributed by NM, 21-Jun-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 453 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 9 1  |-  ( ph  /\ 
ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  pm4.87  592  dfbi  639  mp4an  684  3pm3.2i  1192  unssi  3621  ssini  3667  bm1.3ii  4542  epelg  4765  elvv  4912  funpr  5652  funcnvpr  5658  mpt2v  6413  caovcom  6493  1st2val  6846  2nd2val  6847  elxp7  6853  wfrlem13  7074  wfr3  7082  tfr1a  7138  oeoa  7324  oeoe  7326  erov  7486  endisj  7685  phplem2  7778  snopfsupp  7932  r1funlim  8263  dfac2  8587  cflecard  8709  canth4  9098  canthnumlem  9099  canthwelem  9101  canthp1lem2  9104  pwfseqlem4  9113  wunex3  9192  addsrpr  9525  mulsrpr  9526  recexsrlem  9553  mulcani  10279  div1  10327  recdiv  10341  divdiv1  10346  divdiv2  10347  div23i  10393  div11i  10394  divmuldivi  10395  divadddivi  10397  divdivdivi  10398  lemulge11  10495  negiso  10615  dfnn3  10651  2cnne0  10853  2rene0  10854  halfpm6th  10863  avglt1  10879  avglt2  10880  x2times  11614  xrsupsslem  11621  xrinfmsslem  11622  om2uzoi  12201  fzennn  12213  expge1  12341  faclbnd2  12508  faclbnd4lem1  12510  4bc2eq6  12546  hashf  12554  hashsnlei  12625  hashunlei  12630  hashsslei  12631  hash2prb  12666  repswccat  12925  cshwsexa  12960  funcnvs4  13046  f1oun2prg  13048  wrdlen2i  13067  relexpaddg  13165  cjreb  13235  sqrt2gt1lt2  13387  abs1m  13447  amgm2  13481  climcndslem2  13957  fprodn0f  14094  bpoly3  14160  efcllem  14181  ege2le3  14193  efi4p  14240  efival  14255  sin01bnd  14288  cos01bnd  14289  cos1bnd  14290  cos2bnd  14291  sin01gt0  14293  cos01gt0  14294  sin02gt0  14295  sincos2sgn  14297  sin4lt0  14298  egt2lt3  14307  rpnnen2lem3  14318  rpnnen2lem11  14326  nthruc  14352  nthruz  14353  divalglem5OLD  14425  divalglem5  14426  ndvdsi  14440  bitsp1o  14455  3lcm2e6woprm  14629  6lcm4e12  14630  pcrec  14857  prmrec  14915  prmo1  15044  prmgaplcmlem1  15058  prmgaplcmlem1OLD  15061  prmgaplcm  15080  modsubi  15093  structfn  15183  strlemor0  15265  strlemor1  15266  strleun  15269  isofn  15729  sscres  15777  funcestrcsetclem7  16080  funcestrcsetclem8  16081  fullestrcsetc  16085  mgmnsgrpex  16714  ga0  17001  symg2bas  17088  f1otrspeq  17137  psgnsn  17210  0frgp  17478  gsummptnn0fz  17664  srgbinomlem4  17825  psrbag0  18766  psrbagsn  18767  coe1fsupp  18856  coe1mul2  18911  evls1sca  18961  cnfld1  19042  cnsubdrglem  19068  expmhm  19085  expghm  19116  matmulr  19512  mat1dimelbas  19545  mat1f1o  19552  m2detleib  19705  smadiadetglem1  19745  pmatcollpw3fi1lem2  19860  cpmidpmatlem2  19944  cpmadumatpolylem1  19954  cayhamlem3  19960  cayhamlem4  19961  isbasis3g  20013  fctop  20068  cctop  20070  refref  20577  bl2in  21464  dscmet  21636  iihalf1  22008  iihalf2  22010  icopnfhmeo  22020  iccpnfhmeo  22022  xrhmeo  22023  minveclem2  22417  minveclem4  22423  minveclem2OLD  22429  minveclem4OLD  22435  ovolunlem1a  22498  volf  22532  i1f1lem  22696  mbfi1fseqlem5  22726  dveflem  22980  pilem2  23456  pilem2OLD  23457  pilem3  23458  pilem3OLD  23459  sinhalfpilem  23467  sincosq1lem  23501  tangtx  23509  sinq12gt0  23511  sincos4thpi  23517  sincos6thpi  23519  sincos3rdpi  23520  pige3  23521  coseq1  23526  efeq1  23527  efif1olem4  23543  logblog  23778  angneg  23781  ang180lem1  23787  1cubrlem  23816  quart1  23831  log2cnv  23919  log2tlbnd  23920  log2ublem1  23921  log2ub  23924  emcllem1  23970  emcllem6  23975  basellem1  24056  basellem2  24057  basellem3  24058  basellem8  24063  ppiublem1  24179  ppiublem2  24180  ppiub  24181  chtublem  24188  chtub  24189  bcmono  24254  bclbnd  24257  bpos1lem  24259  bposlem1  24261  bposlem2  24262  bposlem3  24263  bposlem4  24264  bposlem5  24265  bposlem6  24266  bposlem7  24267  bposlem8  24268  bposlem9  24269  lgsdir2lem1  24300  chebbnd1lem1  24356  chebbnd1lem3  24358  chebbnd1  24359  dchrisum0flblem2  24396  dchrisum0lem1  24403  mulog2sumlem2  24422  selberglem2  24433  chpdifbndlem1  24440  ercgrg  24611  axlowdimlem4  25024  axlowdimlem5  25025  axlowdimlem6  25026  axlowdimlem7  25027  axlowdimlem8  25028  axlowdimlem10  25030  axlowdimlem11  25031  usgraexmplvtxlem  25171  usgraexmpldifpr  25176  usgraexmpledg  25180  wlkcomp  25302  0trl  25325  2trllemH  25331  2trllemE  25332  2wlklemA  25333  2wlklemB  25334  2wlklemC  25335  wlkntrllem2  25339  wlkntrl  25341  0pth  25349  0pthonv  25360  constr1trl  25367  1pthon  25370  1pthon2v  25372  constr2spth  25379  constr2pth  25380  2pthon  25381  2pthon3v  25383  usgra2adedgspth  25390  usgra2adedgwlk  25391  usgra2adedgwlkon  25392  usg2wlk  25394  usg2wlkon  25395  usgra2wlkspthlem1  25396  usgra2wlkspthlem2  25397  constr3lem1  25422  constr3lem4  25424  constr3trllem3  25429  constr3pthlem2  25433  clwlkcomp  25540  el2wlkonot  25646  el2spthonot  25647  el2spthonot0  25648  usg2wlkonot  25660  usg2wotspth  25661  frgrancvvdgeq  25820  numclwwlk1  25875  numclwwlk2lem3  25883  frgraregord013  25895  ex-natded5.2i  25905  ex-an  25921  ex-id  25933  ex-po  25934  ex-fl  25946  cnrngo  26180  nvz0  26346  ipidsq  26398  ipdirilem  26519  siilem1  26541  minvecolem2  26566  minvecolem3  26567  minvecolem4  26571  minvecolem2OLD  26576  minvecolem3OLD  26577  minvecolem4OLD  26581  hvsubcan  26776  hvsubcan2  26777  normlem7tALT  26821  helch  26945  hsn0elch  26950  hhshsslem2  26968  hhsssh  26969  shscli  27019  shintcli  27031  shintcl  27032  chintcli  27033  chintcl  27034  shincli  27064  shsval2i  27089  omlsi  27106  chincli  27162  chabs1  27218  fh1i  27323  fh2i  27324  cm2ji  27327  pjnormi  27423  nmopsetn0  27567  nmfnsetn0  27580  lnophm  27721  nmcexi  27728  nmbdfnlb  27752  imaelshi  27760  nlelshi  27762  nmopadjlem  27791  nmopcoadji  27803  hmopidmch  27855  hmopidmpj  27856  sto1i  27938  stlei  27942  stji1i  27944  csmdsymi  28036  chirred  28097  cdj3lem1  28136  xrsclat  28491  nn0archi  28655  lmatfvlem  28690  xrge0iifmhm  28794  qqh0  28837  qqh1  28838  rerrext  28862  cnrrext  28863  prsiga  29002  oms0  29174  oms0OLD  29178  coinfliprv  29364  ballotlem1  29368  ballotth  29419  ballotthOLD  29457  signsw0g  29494  subfacval2  29959  erdszelem2  29964  cvmliftlem4  30060  elmrsubrn  30207  msubfval  30211  problem4  30349  quad3  30351  dfpo2  30444  br6  30446  dfon2lem3  30480  poseq  30540  fullfunfnv  30762  fneref  31055  filnetlem2  31084  filnetlem3  31085  onpsstopbas  31139  bj-2upln1upl  31663  bj-vtoclgfALT  31670  taupilem1  31767  topdifinf  31797  sin2h  31980  cos2h  31981  tan2h  31982  pigt3  31983  poimirlem1  31986  poimirlem2  31987  poimirlem3  31988  poimirlem4  31989  poimirlem6  31991  poimirlem7  31992  poimirlem11  31996  poimirlem12  31997  poimirlem16  32001  poimirlem17  32002  poimirlem19  32004  poimirlem20  32005  poimirlem22  32007  poimirlem23  32008  poimirlem24  32009  poimirlem25  32010  poimirlem26  32011  poimirlem29  32014  poimirlem31  32016  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  dvtanlemOLD  32036  itg2addnclem2  32039  asindmre  32072  heiborlem7  32194  riscer  32272  ac6s6f  32461  ishlatiN  32966  0psubN  33359  atpsubN  33363  mzpclall  35614  diophin  35660  diophun  35661  eldioph4b  35699  irrapx1  35717  2nn0ind  35838  aomclem4  35960  ifpid3g  36181  ifpid2g  36182  ifpbi1b  36192  pwinfi  36213  rtrclex  36269  cnvrcl0  36277  dfrcl2  36311  relexp1idm  36351  relexp0idm  36352  lhe4.4ex1a  36722  expgrowth  36728  ax6e2nd  36969  uun0.1  37205  relopabVD  37338  ax6e2ndVD  37345  sb5ALTVD  37350  ax6e2ndALT  37367  fnchoice  37390  elini  37418  dvmptconst  37823  dvmptidg  37825  dvmulcncf  37835  dvdivcncf  37837  dvnprodlem3  37861  itgsinexplem1  37868  stoweidlem13  37911  stoweidlem14  37912  stoweidlem26  37924  stoweidlem34  37933  stoweidlem49  37948  stoweidlem59  37958  dirkertrigeqlem3  38000  dirkercncflem1  38003  dirkercncflem2  38004  fourierdlem57  38065  fourierdlem62  38070  fourierdlem103  38111  fourierdlem111  38119  fourierswlem  38132  fouriersw  38133  salexct2  38236  salexct3  38239  salgencntex  38240  salgensscntex  38241  gsumge0cl  38251  sge00  38256  sge0tsms  38260  0ome  38388  ovnlecvr  38418  ovn0lem  38425  hoidmvle  38460  astbstanbst  38534  aistbistaandb  38535  abnotataxb  38542  aifftbifffaibif  38547  confun4  38568  plcofph  38570  plvcofph  38572  plvcofphax  38573  plvofpos  38574  mdandyv0  38575  mdandyv1  38576  mdandyv2  38577  mdandyv3  38578  mdandyv4  38579  mdandyv5  38580  mdandyv6  38581  mdandyv7  38582  mdandyv8  38583  mdandyv9  38584  mdandyv10  38585  mdandyv11  38586  mdandyv12  38587  mdandyv13  38588  mdandyv14  38589  mdandyv15  38590  mdandyvr0  38591  mdandyvr1  38592  mdandyvr2  38593  mdandyvr3  38594  mdandyvr4  38595  mdandyvr5  38596  mdandyvr6  38597  mdandyvr7  38598  mdandyvrx0  38607  mdandyvrx1  38608  mdandyvrx2  38609  mdandyvrx3  38610  mdandyvrx4  38611  mdandyvrx5  38612  mdandyvrx6  38613  mdandyvrx7  38614  dandysum2p2e4  38624  mod2eq1n2dvds  38763  zofldiv2ALTV  38829  gbegt5  38900  gbogt5  38901  gboage9  38903  9gboa  38913  11gboa  38914  nnsum3primes4  38921  nnsum3primesgbe  38925  nnsum4primesodd  38929  nnsum4primesoddALTV  38930  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  tgblthelfgott  38946  tgoldbach  38949  41prothprmlem2  38956  pfx2  38993  mptmpt2opabbrd  39076  structvtxvallem  39168  graop  39177  grastruct  39178  uhgrunop  39215  usgrop  39298  usgredgaleordALT  39361  usgr2v1e2w  39377  usgrexmpledg  39384  uhgrsubgrself  39402  uhgrspan1lem1  39422  upgrres1lem1  39426  fusgrfis  39446  nbedgusgr  39496  vtxdushgrfvedglem  39592  vtxdushgrfvedg  39593  uhgrvd0nedgb  39595  umgr2v2e  39612  1wlkcomp  39692  upgr2pthnlp  39765  clWlkcomp  39805  uspgrn2crct  39826  0ewlk  39828  0pth-av  39841  0pthonv-av  39845  1pthon2v-av  39868  21wlkond  39886  2trlond  39888  2pthond  39891  2pthon3v-av  39892  umgr2adedgwlkonALT  39896  umgr2wlk  39898  umgr2wlkon  39899  31wlkdlem4  39903  3trlond  39914  3pthond  39916  3spthond  39918  usgra2pthspth  39938  usgra2pthlem1  39940  isfusgracl  40011  isfusgraclALT  40013  usgo0fis  40023  usgo0fisALT  40024  usgresvm1  40028  usgresvm1ALT  40032  mgmplusgiopALT  40103  sgrp2sgrp  40137  isrnghm  40165  2zrngaabl  40217  rnghmsscmap2  40248  rnghmsscmap  40249  funcrngcsetc  40273  funcrngcsetcALT  40274  rhmsscmap2  40294  rhmsscmap  40295  funcringcsetc  40310  funcringcsetcALTV2lem8  40318  funcringcsetclem8ALTV  40341  zlmodzxzlmod  40408  zlmodzxzel  40409  zlmodzxzscm  40411  zlmodzxzadd  40412  snlindsntorlem  40536  ldepspr  40539  lmod1lem2  40554  lmod1lem3  40555  lmod1lem4  40556  lmod1lem5  40557  lmodn0  40561  zlmodzxznm  40563  zlmodzxzldeplem  40564  zlmodzxzldeplem1  40566  zlmodzxzldeplem3  40568  lvecpsslmod  40573  ldepsnlinc  40574  ldepslinc  40575  divlt1lt  40583  expnegico01  40588  3halfnz  40590  nno  40601  zofldiv2  40611  flnn0div2ge  40613  elbigo2  40636  nnlog2ge0lt1  40650  digfval  40681  dignnld  40687  dignn0flhalf  40702  dpfrac1  40765  alimp-surprise  40792  aacllem  40813
  Copyright terms: Public domain W3C validator