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  3647  ssini  3691  bm1.3ii  4551  epelg  4766  elvv  4913  funpr  5652  mpt2v  6400  caovcom  6480  1st2val  6833  2nd2val  6834  elxp7  6840  wfrlem13  7056  wfr3  7064  tfr1a  7120  oeoa  7306  oeoe  7308  erov  7468  endisj  7665  phplem2  7758  snopfsupp  7912  r1funlim  8236  dfac2  8559  cflecard  8681  canth4  9071  canthnumlem  9072  canthwelem  9074  canthp1lem2  9077  pwfseqlem4  9086  wunex3  9165  addsrpr  9498  mulsrpr  9499  recexsrlem  9526  mulcani  10250  div1  10298  recdiv  10312  divdiv1  10317  divdiv2  10318  div23i  10364  div11i  10365  divmuldivi  10366  divadddivi  10368  divdivdivi  10369  lemulge11  10466  negiso  10587  dfnn3  10623  2cnne0  10824  2rene0  10825  halfpm6th  10834  avglt1  10850  avglt2  10851  x2times  11585  xrsupsslem  11592  xrinfmsslem  11593  injresinjlem  12021  om2uzoi  12166  fzennn  12178  expge1  12306  faclbnd2  12473  faclbnd4lem1  12475  4bc2eq6  12511  hashf  12519  hashsnlei  12587  hashunlei  12592  hashsslei  12593  hash2prd  12627  hash2prv  12634  repswccat  12873  cshwsexa  12908  f1oun2prg  12981  wrdlen2i  13000  relexpaddg  13095  cjreb  13165  sqrt2gt1lt2  13317  abs1m  13377  amgm2  13411  climcndslem2  13886  fprodn0f  14023  bpoly3  14089  efcllem  14110  ege2le3  14122  efi4p  14169  efival  14184  sin01bnd  14217  cos01bnd  14218  cos1bnd  14219  cos2bnd  14220  cos01gt0  14223  sin02gt0  14224  sincos2sgn  14226  sin4lt0  14227  egt2lt3  14236  rpnnen2lem3  14247  rpnnen2lem11  14255  nthruc  14281  nthruz  14282  divalglem5  14353  ndvdsi  14366  bitsp1o  14381  3lcm2e6woprm  14551  6lcm4e12  14552  pcrec  14771  prmrec  14829  prmo1  14958  prmgaplcmlem1  14972  prmgaplcmlem1OLD  14975  prmgaplcm  14994  modsubi  15007  structfn  15097  strlemor0  15178  strlemor1  15179  strleun  15182  isofn  15631  sscres  15679  funcestrcsetclem7  15982  funcestrcsetclem8  15983  fullestrcsetc  15987  mgmnsgrpex  16616  ga0  16903  symg2bas  16990  f1otrspeq  17039  psgnsn  17112  0frgp  17364  gsummptnn0fz  17550  srgbinomlem4  17711  psrbag0  18652  psrbagsn  18653  coe1fsupp  18742  coe1mul2  18797  evls1sca  18847  cnfld1  18928  cnsubdrglem  18954  expmhm  18970  expghm  18998  matmulr  19394  mat1dimelbas  19427  mat1f1o  19434  m2detleib  19587  smadiadetglem1  19627  pmatcollpw3fi1lem2  19742  cpmidpmatlem2  19826  cpmadumatpolylem1  19836  cayhamlem3  19842  cayhamlem4  19843  isbasis3g  19895  fctop  19950  cctop  19952  refref  20459  bl2in  21346  dscmet  21518  iihalf1  21855  iihalf2  21857  icopnfhmeo  21867  iccpnfhmeo  21869  xrhmeo  21870  minveclem2  22261  minveclem4  22267  ovolunlem1a  22327  volf  22360  i1f1lem  22524  mbfi1fseqlem5  22554  dveflem  22808  pilem2  23272  pilem2OLD  23273  pilem3  23274  pilem3OLD  23275  sinhalfpilem  23283  sincosq1lem  23317  tangtx  23325  sinq12gt0  23327  sincos4thpi  23333  sincos6thpi  23335  sincos3rdpi  23336  pige3  23337  coseq1  23342  efeq1  23343  efif1olem4  23359  logblog  23594  angneg  23597  ang180lem1  23603  1cubrlem  23632  quart1  23647  log2cnv  23735  log2tlbnd  23736  log2ublem1  23737  log2ub  23740  emcllem1  23786  emcllem6  23791  basellem1  23870  basellem2  23871  basellem3  23872  basellem8  23877  ppiublem1  23993  ppiublem2  23994  ppiub  23995  chtublem  24002  chtub  24003  bcmono  24068  bclbnd  24071  bpos1lem  24073  bposlem1  24075  bposlem2  24076  bposlem3  24077  bposlem4  24078  bposlem5  24079  bposlem6  24080  bposlem7  24081  bposlem8  24082  bposlem9  24083  lgsdir2lem1  24114  chebbnd1lem1  24170  chebbnd1lem3  24172  chebbnd1  24173  dchrisum0flblem2  24210  dchrisum0lem1  24217  mulog2sumlem2  24236  selberglem2  24247  chpdifbndlem1  24254  ercgrg  24424  axlowdimlem4  24821  axlowdimlem5  24822  axlowdimlem6  24823  axlowdimlem7  24824  axlowdimlem8  24825  axlowdimlem10  24827  axlowdimlem11  24828  usgraexvlem  24968  usgraexmpldifpr  24973  usgraexmpledg  24976  wlkcomp  25098  0trl  25121  2trllemH  25127  2trllemE  25128  2wlklemA  25129  2wlklemB  25130  2wlklemC  25131  wlkntrllem2  25135  wlkntrl  25137  0pth  25145  0pthonv  25156  constr1trl  25163  1pthon  25166  1pthon2v  25168  constr2spth  25175  constr2pth  25176  2pthon  25177  2pthon3v  25179  usgra2adedgspth  25186  usgra2adedgwlk  25187  usgra2adedgwlkon  25188  usg2wlk  25190  usg2wlkon  25191  usgra2wlkspthlem1  25192  usgra2wlkspthlem2  25193  constr3lem1  25218  constr3lem4  25220  constr3trllem3  25225  constr3pthlem2  25229  clwlkcomp  25336  el2wlkonot  25442  el2spthonot  25443  el2spthonot0  25444  usg2wlkonot  25456  usg2wotspth  25457  frgrancvvdgeq  25616  numclwwlk1  25671  numclwwlk2lem3  25679  frgraregord013  25691  ex-natded5.2i  25701  ex-an  25717  ex-id  25729  ex-po  25730  ex-fl  25742  cnrngo  25976  nvz0  26142  ipidsq  26194  ipdirilem  26315  siilem1  26337  minvecolem2  26362  minvecolem3  26363  minvecolem4  26367  hvsubcan  26562  hvsubcan2  26563  normlem7tALT  26607  helch  26731  hsn0elch  26736  hhshsslem2  26754  hhsssh  26755  shscli  26805  shintcli  26817  shintcl  26818  chintcli  26819  chintcl  26820  shincli  26850  shsval2i  26875  omlsi  26892  chincli  26948  chabs1  27004  fh1i  27109  fh2i  27110  cm2ji  27113  pjnormi  27209  nmopsetn0  27353  nmfnsetn0  27366  lnophm  27507  nmcexi  27514  nmbdfnlb  27538  imaelshi  27546  nlelshi  27548  nmopadjlem  27577  nmopcoadji  27589  hmopidmch  27641  hmopidmpj  27642  sto1i  27724  stlei  27728  stji1i  27730  csmdsymi  27822  chirred  27883  cdj3lem1  27922  xrsclat  28279  nn0archi  28445  lmatfvlem  28480  xrge0iifmhm  28584  qqh0  28627  qqh1  28628  rerrext  28652  cnrrext  28653  prsiga  28792  oms0  28958  coinfliprv  29141  ballotlem1  29145  ballotth  29196  signsw0g  29233  subfacval2  29698  erdszelem2  29703  cvmliftlem4  29799  elmrsubrn  29946  msubfval  29950  problem4  30088  quad3  30090  dfpo2  30182  br6  30184  dfon2lem3  30218  poseq  30278  fullfunfnv  30498  fneref  30791  filnetlem2  30820  filnetlem3  30821  onpsstopbas  30875  bj-2upln1upl  31367  bj-vtoclgfALT  31373  taupilem1  31467  topdifinf  31486  sin2h  31638  cos2h  31639  tan2h  31640  pigt3  31641  poimirlem1  31644  poimirlem2  31645  poimirlem3  31646  poimirlem4  31647  poimirlem6  31649  poimirlem7  31650  poimirlem11  31654  poimirlem12  31655  poimirlem16  31659  poimirlem17  31660  poimirlem19  31662  poimirlem20  31663  poimirlem22  31665  poimirlem23  31666  poimirlem24  31667  poimirlem25  31668  poimirlem26  31669  poimirlem29  31672  poimirlem31  31674  mblfinlem3  31682  mblfinlem4  31683  ismblfin  31684  dvtanlemOLD  31694  itg2addnclem2  31697  asindmre  31730  heiborlem7  31852  riscer  31930  ac6s6f  32119  ishlatiN  32629  0psubN  33022  atpsubN  33026  mzpclall  35277  diophin  35323  diophun  35324  eldioph4b  35362  irrapx1  35381  2nn0ind  35498  aomclem4  35620  ifpid3g  35834  ifpid2g  35835  ifpbi1b  35845  pwinfi  35866  dfrcl2  35904  relexp1idm  35944  relexp0idm  35945  lhe4.4ex1a  36314  expgrowth  36320  ax6e2nd  36561  uun0.1  36804  relopabVD  36937  ax6e2ndVD  36944  sb5ALTVD  36949  ax6e2ndALT  36966  fnchoice  36989  elini  37019  dvmptconst  37356  dvmptidg  37358  dvmulcncf  37368  dvdivcncf  37370  dvnprodlem3  37391  itgsinexplem1  37398  stoweidlem13  37441  stoweidlem14  37442  stoweidlem26  37454  stoweidlem34  37463  stoweidlem49  37478  stoweidlem59  37488  dirkertrigeqlem3  37530  dirkercncflem1  37533  dirkercncflem2  37534  fourierdlem57  37594  fourierdlem62  37599  fourierdlem103  37640  fourierdlem111  37648  fourierswlem  37661  fouriersw  37662  gsumge0cl  37746  sge00  37751  sge0tsms  37755  astbstanbst  37895  aistbistaandb  37896  abnotataxb  37903  aifftbifffaibif  37908  confun4  37922  plcofph  37924  plvcofph  37926  mdandyv0  37927  mdandyv1  37928  mdandyv2  37929  mdandyv3  37930  mdandyv4  37931  mdandyv5  37932  mdandyv6  37933  mdandyv7  37934  mdandyv8  37935  mdandyv9  37936  mdandyv10  37937  mdandyv11  37938  mdandyv12  37939  mdandyv13  37940  mdandyv14  37941  mdandyv15  37942  mdandyvr0  37943  mdandyvr1  37944  mdandyvr2  37945  mdandyvr3  37946  mdandyvr4  37947  mdandyvr5  37948  mdandyvr6  37949  mdandyvr7  37950  mdandyvrx0  37959  mdandyvrx1  37960  mdandyvrx2  37961  mdandyvrx3  37962  mdandyvrx4  37963  mdandyvrx5  37964  mdandyvrx6  37965  mdandyvrx7  37966  dandysum2p2e4  37976  mod2eq1n2dvds  38114  zofldiv2ALTV  38180  gbegt5  38251  gbogt5  38252  gboage9  38254  9gboa  38264  11gboa  38265  nnsum3primes4  38272  nnsum3primesgbe  38276  nnsum4primesodd  38280  nnsum4primesoddALTV  38281  nnsum4primeseven  38284  nnsum4primesevenALTV  38285  tgblthelfgott  38297  tgoldbach  38300  41prothprmlem2  38307  pfx2  38342  usgra2pthspth  38420  usgra2pthlem1  38422  isfusgracl  38495  isfusgraclALT  38497  usgo0fis  38507  usgo0fisALT  38508  usgresvm1  38512  usgresvm1ALT  38516  mgmplusgiopALT  38587  sgrp2sgrp  38621  isrnghm  38649  2zrngaabl  38701  rnghmsscmap2  38732  rnghmsscmap  38733  funcrngcsetc  38757  funcrngcsetcALT  38758  rhmsscmap2  38778  rhmsscmap  38779  funcringcsetc  38794  funcringcsetcALTV2lem8  38802  funcringcsetclem8ALTV  38825  zlmodzxzlmod  38894  zlmodzxzel  38895  zlmodzxzscm  38897  zlmodzxzadd  38898  snlindsntorlem  39022  ldepspr  39025  lmod1lem2  39040  lmod1lem3  39041  lmod1lem4  39042  lmod1lem5  39043  lmodn0  39047  zlmodzxznm  39049  zlmodzxzldeplem  39050  zlmodzxzldeplem1  39052  zlmodzxzldeplem3  39054  lvecpsslmod  39059  ldepsnlinc  39060  ldepslinc  39061  divlt1lt  39069  expnegico01  39074  3halfnz  39077  nno  39088  zofldiv2  39098  flnn0div2ge  39100  elbigo2  39123  nnlog2ge0lt1  39137  digfval  39168  dignnld  39174  dignn0flhalf  39189  dpfrac1  39252  alimp-surprise  39279  aacllem  39300
  Copyright terms: Public domain W3C validator