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

Theorem pm3.2i 456
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 448 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 9 1  |-  ( ph  /\ 
ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm4.87  586  dfbi  633  mp4an  677  3pm3.2i  1183  unssi  3641  ssini  3685  bm1.3ii  4549  epelg  4765  elvv  4912  funpr  5652  mpt2v  6400  caovcom  6480  1st2val  6833  2nd2val  6834  elxp7  6840  wfrlem13  7059  wfr3  7067  tfr1a  7123  oeoa  7309  oeoe  7311  erov  7471  endisj  7668  phplem2  7761  snopfsupp  7915  r1funlim  8245  dfac2  8568  cflecard  8690  canth4  9079  canthnumlem  9080  canthwelem  9082  canthp1lem2  9085  pwfseqlem4  9094  wunex3  9173  addsrpr  9506  mulsrpr  9507  recexsrlem  9534  mulcani  10258  div1  10306  recdiv  10320  divdiv1  10325  divdiv2  10326  div23i  10372  div11i  10373  divmuldivi  10374  divadddivi  10376  divdivdivi  10377  lemulge11  10474  negiso  10594  dfnn3  10630  2cnne0  10831  2rene0  10832  halfpm6th  10841  avglt1  10857  avglt2  10858  x2times  11592  xrsupsslem  11599  xrinfmsslem  11600  injresinjlem  12030  om2uzoi  12175  fzennn  12187  expge1  12315  faclbnd2  12482  faclbnd4lem1  12484  4bc2eq6  12520  hashf  12528  hashsnlei  12596  hashunlei  12601  hashsslei  12602  hash2prb  12637  repswccat  12890  cshwsexa  12925  f1oun2prg  13002  wrdlen2i  13021  relexpaddg  13116  cjreb  13186  sqrt2gt1lt2  13338  abs1m  13398  amgm2  13432  climcndslem2  13907  fprodn0f  14044  bpoly3  14110  efcllem  14131  ege2le3  14143  efi4p  14190  efival  14205  sin01bnd  14238  cos01bnd  14239  cos1bnd  14240  cos2bnd  14241  sin01gt0  14243  cos01gt0  14244  sin02gt0  14245  sincos2sgn  14247  sin4lt0  14248  egt2lt3  14257  rpnnen2lem3  14268  rpnnen2lem11  14276  nthruc  14302  nthruz  14303  divalglem5OLD  14375  divalglem5  14376  ndvdsi  14390  bitsp1o  14405  3lcm2e6woprm  14579  6lcm4e12  14580  pcrec  14807  prmrec  14865  prmo1  14994  prmgaplcmlem1  15008  prmgaplcmlem1OLD  15011  prmgaplcm  15030  modsubi  15043  structfn  15133  strlemor0  15215  strlemor1  15216  strleun  15219  isofn  15679  sscres  15727  funcestrcsetclem7  16030  funcestrcsetclem8  16031  fullestrcsetc  16035  mgmnsgrpex  16664  ga0  16951  symg2bas  17038  f1otrspeq  17087  psgnsn  17160  0frgp  17428  gsummptnn0fz  17614  srgbinomlem4  17775  psrbag0  18716  psrbagsn  18717  coe1fsupp  18806  coe1mul2  18861  evls1sca  18911  cnfld1  18992  cnsubdrglem  19018  expmhm  19034  expghm  19065  matmulr  19461  mat1dimelbas  19494  mat1f1o  19501  m2detleib  19654  smadiadetglem1  19694  pmatcollpw3fi1lem2  19809  cpmidpmatlem2  19893  cpmadumatpolylem1  19903  cayhamlem3  19909  cayhamlem4  19910  isbasis3g  19962  fctop  20017  cctop  20019  refref  20526  bl2in  21413  dscmet  21585  iihalf1  21957  iihalf2  21959  icopnfhmeo  21969  iccpnfhmeo  21971  xrhmeo  21972  minveclem2  22366  minveclem4  22372  minveclem2OLD  22378  minveclem4OLD  22384  ovolunlem1a  22447  volf  22481  i1f1lem  22645  mbfi1fseqlem5  22675  dveflem  22929  pilem2  23405  pilem2OLD  23406  pilem3  23407  pilem3OLD  23408  sinhalfpilem  23416  sincosq1lem  23450  tangtx  23458  sinq12gt0  23460  sincos4thpi  23466  sincos6thpi  23468  sincos3rdpi  23469  pige3  23470  coseq1  23475  efeq1  23476  efif1olem4  23492  logblog  23727  angneg  23730  ang180lem1  23736  1cubrlem  23765  quart1  23780  log2cnv  23868  log2tlbnd  23869  log2ublem1  23870  log2ub  23873  emcllem1  23919  emcllem6  23924  basellem1  24005  basellem2  24006  basellem3  24007  basellem8  24012  ppiublem1  24128  ppiublem2  24129  ppiub  24130  chtublem  24137  chtub  24138  bcmono  24203  bclbnd  24206  bpos1lem  24208  bposlem1  24210  bposlem2  24211  bposlem3  24212  bposlem4  24213  bposlem5  24214  bposlem6  24215  bposlem7  24216  bposlem8  24217  bposlem9  24218  lgsdir2lem1  24249  chebbnd1lem1  24305  chebbnd1lem3  24307  chebbnd1  24308  dchrisum0flblem2  24345  dchrisum0lem1  24352  mulog2sumlem2  24371  selberglem2  24382  chpdifbndlem1  24389  ercgrg  24560  axlowdimlem4  24973  axlowdimlem5  24974  axlowdimlem6  24975  axlowdimlem7  24976  axlowdimlem8  24977  axlowdimlem10  24979  axlowdimlem11  24980  usgraexmplvtxlem  25120  usgraexmpldifpr  25125  usgraexmpledg  25129  wlkcomp  25251  0trl  25274  2trllemH  25280  2trllemE  25281  2wlklemA  25282  2wlklemB  25283  2wlklemC  25284  wlkntrllem2  25288  wlkntrl  25290  0pth  25298  0pthonv  25309  constr1trl  25316  1pthon  25319  1pthon2v  25321  constr2spth  25328  constr2pth  25329  2pthon  25330  2pthon3v  25332  usgra2adedgspth  25339  usgra2adedgwlk  25340  usgra2adedgwlkon  25341  usg2wlk  25343  usg2wlkon  25344  usgra2wlkspthlem1  25345  usgra2wlkspthlem2  25346  constr3lem1  25371  constr3lem4  25373  constr3trllem3  25378  constr3pthlem2  25382  clwlkcomp  25489  el2wlkonot  25595  el2spthonot  25596  el2spthonot0  25597  usg2wlkonot  25609  usg2wotspth  25610  frgrancvvdgeq  25769  numclwwlk1  25824  numclwwlk2lem3  25832  frgraregord013  25844  ex-natded5.2i  25854  ex-an  25870  ex-id  25882  ex-po  25883  ex-fl  25895  cnrngo  26129  nvz0  26295  ipidsq  26347  ipdirilem  26468  siilem1  26490  minvecolem2  26515  minvecolem3  26516  minvecolem4  26520  minvecolem2OLD  26525  minvecolem3OLD  26526  minvecolem4OLD  26530  hvsubcan  26725  hvsubcan2  26726  normlem7tALT  26770  helch  26894  hsn0elch  26899  hhshsslem2  26917  hhsssh  26918  shscli  26968  shintcli  26980  shintcl  26981  chintcli  26982  chintcl  26983  shincli  27013  shsval2i  27038  omlsi  27055  chincli  27111  chabs1  27167  fh1i  27272  fh2i  27273  cm2ji  27276  pjnormi  27372  nmopsetn0  27516  nmfnsetn0  27529  lnophm  27670  nmcexi  27677  nmbdfnlb  27701  imaelshi  27709  nlelshi  27711  nmopadjlem  27740  nmopcoadji  27752  hmopidmch  27804  hmopidmpj  27805  sto1i  27887  stlei  27891  stji1i  27893  csmdsymi  27985  chirred  28046  cdj3lem1  28085  xrsclat  28449  nn0archi  28614  lmatfvlem  28649  xrge0iifmhm  28753  qqh0  28796  qqh1  28797  rerrext  28821  cnrrext  28822  prsiga  28961  oms0  29133  oms0OLD  29137  coinfliprv  29323  ballotlem1  29327  ballotth  29378  ballotthOLD  29416  signsw0g  29453  subfacval2  29918  erdszelem2  29923  cvmliftlem4  30019  elmrsubrn  30166  msubfval  30170  problem4  30308  quad3  30310  dfpo2  30402  br6  30404  dfon2lem3  30438  poseq  30498  fullfunfnv  30718  fneref  31011  filnetlem2  31040  filnetlem3  31041  onpsstopbas  31095  bj-2upln1upl  31586  bj-vtoclgfALT  31592  taupilem1  31686  topdifinf  31716  sin2h  31899  cos2h  31900  tan2h  31901  pigt3  31902  poimirlem1  31905  poimirlem2  31906  poimirlem3  31907  poimirlem4  31908  poimirlem6  31910  poimirlem7  31911  poimirlem11  31915  poimirlem12  31916  poimirlem16  31920  poimirlem17  31921  poimirlem19  31923  poimirlem20  31924  poimirlem22  31926  poimirlem23  31927  poimirlem24  31928  poimirlem25  31929  poimirlem26  31930  poimirlem29  31933  poimirlem31  31935  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  dvtanlemOLD  31955  itg2addnclem2  31958  asindmre  31991  heiborlem7  32113  riscer  32191  ac6s6f  32380  ishlatiN  32890  0psubN  33283  atpsubN  33287  mzpclall  35538  diophin  35584  diophun  35585  eldioph4b  35623  irrapx1  35642  2nn0ind  35763  aomclem4  35885  ifpid3g  36106  ifpid2g  36107  ifpbi1b  36117  pwinfi  36138  rtrclex  36194  cnvrcl0  36202  dfrcl2  36236  relexp1idm  36276  relexp0idm  36277  lhe4.4ex1a  36648  expgrowth  36654  ax6e2nd  36895  uun0.1  37138  relopabVD  37271  ax6e2ndVD  37278  sb5ALTVD  37283  ax6e2ndALT  37300  fnchoice  37323  elini  37353  dvmptconst  37725  dvmptidg  37727  dvmulcncf  37737  dvdivcncf  37739  dvnprodlem3  37763  itgsinexplem1  37770  stoweidlem13  37813  stoweidlem14  37814  stoweidlem26  37826  stoweidlem34  37835  stoweidlem49  37850  stoweidlem59  37860  dirkertrigeqlem3  37902  dirkercncflem1  37905  dirkercncflem2  37906  fourierdlem57  37967  fourierdlem62  37972  fourierdlem103  38013  fourierdlem111  38021  fourierswlem  38034  fouriersw  38035  gsumge0cl  38121  sge00  38126  sge0tsms  38130  0ome  38258  ovnlecvr  38284  ovn0lem  38291  hoidmvle  38326  astbstanbst  38367  aistbistaandb  38368  abnotataxb  38375  aifftbifffaibif  38380  confun4  38401  plcofph  38403  plvcofph  38405  plvcofphax  38406  plvofpos  38407  mdandyv0  38408  mdandyv1  38409  mdandyv2  38410  mdandyv3  38411  mdandyv4  38412  mdandyv5  38413  mdandyv6  38414  mdandyv7  38415  mdandyv8  38416  mdandyv9  38417  mdandyv10  38418  mdandyv11  38419  mdandyv12  38420  mdandyv13  38421  mdandyv14  38422  mdandyv15  38423  mdandyvr0  38424  mdandyvr1  38425  mdandyvr2  38426  mdandyvr3  38427  mdandyvr4  38428  mdandyvr5  38429  mdandyvr6  38430  mdandyvr7  38431  mdandyvrx0  38440  mdandyvrx1  38441  mdandyvrx2  38442  mdandyvrx3  38443  mdandyvrx4  38444  mdandyvrx5  38445  mdandyvrx6  38446  mdandyvrx7  38447  dandysum2p2e4  38457  mod2eq1n2dvds  38595  zofldiv2ALTV  38661  gbegt5  38732  gbogt5  38733  gboage9  38735  9gboa  38745  11gboa  38746  nnsum3primes4  38753  nnsum3primesgbe  38757  nnsum4primesodd  38761  nnsum4primesoddALTV  38762  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  tgblthelfgott  38778  tgoldbach  38781  41prothprmlem2  38788  pfx2  38823  structvtxvallem  38952  graop  38960  grastruct  38961  uhgrunop  38998  usgredgaleord  39091  usgrexmpledg  39110  uhgrsubgrself  39125  uhgrspan1lem1  39141  umgrres1lem1  39145  fusgrfis  39162  usgra2pthspth  39284  usgra2pthlem1  39286  isfusgracl  39357  isfusgraclALT  39359  usgo0fis  39369  usgo0fisALT  39370  usgresvm1  39374  usgresvm1ALT  39378  mgmplusgiopALT  39449  sgrp2sgrp  39483  isrnghm  39511  2zrngaabl  39563  rnghmsscmap2  39594  rnghmsscmap  39595  funcrngcsetc  39619  funcrngcsetcALT  39620  rhmsscmap2  39640  rhmsscmap  39641  funcringcsetc  39656  funcringcsetcALTV2lem8  39664  funcringcsetclem8ALTV  39687  zlmodzxzlmod  39756  zlmodzxzel  39757  zlmodzxzscm  39759  zlmodzxzadd  39760  snlindsntorlem  39884  ldepspr  39887  lmod1lem2  39902  lmod1lem3  39903  lmod1lem4  39904  lmod1lem5  39905  lmodn0  39909  zlmodzxznm  39911  zlmodzxzldeplem  39912  zlmodzxzldeplem1  39914  zlmodzxzldeplem3  39916  lvecpsslmod  39921  ldepsnlinc  39922  ldepslinc  39923  divlt1lt  39931  expnegico01  39936  3halfnz  39938  nno  39949  zofldiv2  39959  flnn0div2ge  39961  elbigo2  39984  nnlog2ge0lt1  39998  digfval  40029  dignnld  40035  dignn0flhalf  40050  dpfrac1  40113  alimp-surprise  40140  aacllem  40161
  Copyright terms: Public domain W3C validator