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

Theorem pm3.2i 455
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 447 . 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  584  dfbi  629  mp4an  673  3pm3.2i  1174  unssi  3679  ssini  3721  bm1.3ii  4571  epelg  4792  elvv  5057  funpr  5637  mpt2v  6374  caovcom  6454  1st2val  6807  2nd2val  6808  elxp7  6814  tfr1a  7060  oeoa  7243  oeoe  7245  erov  7405  endisj  7601  phplem2  7694  snopfsupp  7848  cantnffvalOLD  8078  r1funlim  8180  dfac2  8507  cflecard  8629  canth4  9021  canthnumlem  9022  canthwelem  9024  canthp1lem2  9027  pwfseqlem4  9036  wunex3  9115  addsrpr  9448  mulsrpr  9449  recexsrlem  9476  mulcani  10184  div1  10232  recdiv  10246  divdiv1  10251  divdiv2  10252  div23i  10298  div11i  10299  divmuldivi  10300  divadddivi  10302  divdivdivi  10303  lemulge11  10400  negiso  10515  dfnn3  10546  2cnne0  10746  2rene0  10747  halfpm6th  10756  avglt1  10772  avglt2  10773  x2times  11487  xrsupsslem  11494  xrinfmsslem  11495  injresinjlem  11889  om2uzoi  12030  fzennn  12042  expge1  12167  faclbnd2  12333  faclbnd4lem1  12335  hashf  12376  hashsnlei  12439  hashunlei  12444  hashsslei  12445  hash2prd  12480  hash2prv  12487  lsw0g  12548  repswccat  12716  cshwsexa  12751  f1oun2prg  12824  wrdlen2i  12843  cjreb  12915  sqrt2gt1lt2  13067  abs1m  13127  amgm2  13161  climcndslem2  13621  efcllem  13671  ege2le3  13683  efi4p  13729  efival  13744  sin01bnd  13777  cos01bnd  13778  cos1bnd  13779  cos2bnd  13780  cos01gt0  13783  sin02gt0  13784  sincos2sgn  13786  sin4lt0  13787  egt2lt3  13796  rpnnen2lem3  13807  rpnnen2lem11  13815  nthruc  13841  nthruz  13842  divalglem5  13910  ndvdsi  13923  bitsp1o  13938  pcrec  14237  prmrec  14295  modsubi  14413  structfn  14499  strlemor0  14577  strlemor1  14578  strleun  14581  sscres  15049  ga0  16131  symg2bas  16218  f1otrspeq  16268  psgnsn  16341  0frgp  16593  gsummptnn0fz  16805  srgbinomlem4  16982  psrbag0  17930  psrbagsn  17931  coe1fsupp  18025  coe1mul2  18081  evls1sca  18131  cnfld1  18214  cnsubdrglem  18237  expmhm  18253  expghm  18296  expghmOLD  18297  matmulr  18707  mat1dimelbas  18740  mat1f1o  18747  m2detleib  18900  smadiadetglem1  18940  pmatcollpw3fi1lem2  19055  cpmidpmatlem2  19139  cpmadumatpolylem1  19149  cayhamlem3  19155  cayhamlem4  19156  isbasis3g  19217  fctop  19271  cctop  19273  bl2in  20638  dscmet  20828  iihalf1  21166  iihalf2  21168  icopnfhmeo  21178  iccpnfhmeo  21180  xrhmeo  21181  minveclem2  21576  minveclem4  21582  ovolunlem1a  21642  volf  21675  i1f1lem  21831  mbfi1fseqlem5  21861  dveflem  22115  pilem2  22581  pilem3  22582  sinhalfpilem  22589  sincosq1lem  22623  tangtx  22631  sinq12gt0  22633  sincos4thpi  22639  sincos6thpi  22641  sincos3rdpi  22642  pige3  22643  coseq1  22648  efeq1  22649  efif1olem4  22665  angneg  22863  ang180lem1  22869  1cubrlem  22900  quart1  22915  log2cnv  23003  log2tlbnd  23004  log2ublem1  23005  log2ub  23008  emcllem1  23053  emcllem6  23058  basellem1  23082  basellem2  23083  basellem3  23084  basellem8  23089  ppiublem1  23205  ppiublem2  23206  ppiub  23207  chtublem  23214  chtub  23215  bcmono  23280  bclbnd  23283  bpos1lem  23285  bposlem1  23287  bposlem2  23288  bposlem3  23289  bposlem4  23290  bposlem5  23291  bposlem6  23292  bposlem7  23293  bposlem8  23294  bposlem9  23295  lgsdir2lem1  23326  chebbnd1lem1  23382  chebbnd1lem3  23384  chebbnd1  23385  dchrisum0flblem2  23422  dchrisum0lem1  23429  mulog2sumlem2  23448  selberglem2  23459  chpdifbndlem1  23466  ercgrg  23636  axlowdimlem4  23924  axlowdimlem5  23925  axlowdimlem6  23926  axlowdimlem7  23927  axlowdimlem8  23928  axlowdimlem10  23930  axlowdimlem11  23931  usgraexvlem  24071  usgraexmpldifpr  24076  usgraexmpledg  24079  wlkcomp  24201  0trl  24224  2trllemH  24230  2trllemE  24231  2wlklemA  24232  2wlklemB  24233  2wlklemC  24234  wlkntrllem2  24238  wlkntrl  24240  0pth  24248  0pthonv  24259  constr1trl  24266  1pthon  24269  1pthon2v  24271  constr2spth  24278  constr2pth  24279  2pthon  24280  2pthon3v  24282  usgra2adedgspth  24289  usgra2adedgwlk  24290  usgra2adedgwlkon  24291  usg2wlk  24293  usg2wlkon  24294  usgra2wlkspthlem1  24295  usgra2wlkspthlem2  24296  constr3lem1  24321  constr3lem4  24323  constr3trllem3  24328  constr3pthlem2  24332  clwlkcomp  24439  el2wlkonot  24545  el2spthonot  24546  el2spthonot0  24547  usg2wlkonot  24559  usg2wotspth  24560  frgrancvvdgeq  24720  numclwwlk1  24775  numclwwlk2lem3  24783  frgraregord013  24795  ex-natded5.2i  24804  ex-an  24820  ex-id  24832  ex-po  24833  ex-fl  24845  cnrngo  25081  nvz0  25247  ipidsq  25299  ipdirilem  25420  siilem1  25442  minvecolem2  25467  minvecolem3  25468  minvecolem4  25472  hvsubcan  25667  hvsubcan2  25668  normlem7tALT  25712  helch  25837  hsn0elch  25842  hhshsslem2  25860  hhsssh  25861  shscli  25911  shintcli  25923  shintcl  25924  chintcli  25925  chintcl  25926  shincli  25956  shsval2i  25981  omlsi  25998  chincli  26054  chabs1  26110  fh1i  26215  fh2i  26216  cm2ji  26219  pjnormi  26315  nmopsetn0  26460  nmfnsetn0  26473  lnophm  26614  nmcexi  26621  nmbdfnlb  26645  imaelshi  26653  nlelshi  26655  nmopadjlem  26684  nmopcoadji  26696  hmopidmch  26748  hmopidmpj  26749  sto1i  26831  stlei  26835  stji1i  26837  csmdsymi  26929  chirred  26990  cdj3lem1  27029  xrsclat  27330  reofld  27493  nn0archi  27496  xrge0iifmhm  27557  cnzh  27587  rezh  27588  qqh0  27601  qqh1  27602  rerrext  27626  cnrrext  27627  prsiga  27771  oms0  27906  coinfliprv  28061  ballotlem1  28065  ballotth  28116  signsw0g  28153  signswmnd  28154  subfacval2  28271  erdszelem2  28276  cvmliftlem4  28373  problem4  28497  quad3  28499  4bc2eq6  28587  dfpo2  28761  br6  28763  dfon2lem3  28794  poseq  28910  wfrlem13  28932  wfr3  28938  fullfunfnv  29173  bpoly3  29397  onpsstopbas  29472  sin2h  29622  cos2h  29623  tan2h  29624  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  dvtanlem  29641  itg2addnclem2  29644  asindmre  29679  fneref  29756  refref  29757  filnetlem2  29800  filnetlem3  29801  heiborlem7  29916  riscer  29994  ac6s6f  30185  mzpclall  30263  diophin  30310  diophun  30311  eldioph4b  30349  irrapx1  30368  2nn0ind  30485  aomclem4  30607  lhe4.4ex1a  30834  expgrowth  30840  fnchoice  30982  halffl  31070  sumnnodd  31172  0cnf  31215  icccncfext  31226  cncfiooicclem1  31232  cncfiooicc  31233  cncfiooiccre  31234  dvmptconst  31243  dvmptidg  31245  dvmulcncf  31255  dvdivcncf  31257  itgsinexplem1  31271  iblempty  31283  iblsplit  31284  iblcncfioo  31296  stoweidlem13  31313  stoweidlem14  31314  stoweidlem26  31326  stoweidlem34  31334  stoweidlem49  31349  stoweidlem59  31359  dirker2re  31392  dirkerdenne0  31393  dirkerval2  31394  dirkerre  31395  dirkerper  31396  dirkertrigeqlem1  31398  dirkertrigeqlem3  31400  dirkertrigeq  31401  dirkercncflem1  31403  dirkercncflem2  31404  dirkercncflem4  31406  dirkercncf  31407  fourierdlem24  31431  fourierdlem43  31450  fourierdlem57  31464  fourierdlem58  31465  fourierdlem62  31469  fourierdlem93  31500  fourierdlem103  31510  fourierdlem111  31518  fourierdlem112  31519  sqwvfoura  31529  sqwvfourb  31530  fourierswlem  31531  fouriersw  31532  astbstanbst  31571  aistbistaandb  31572  abnotataxb  31579  mdandyv0  31588  mdandyv1  31589  mdandyv2  31590  mdandyv3  31591  mdandyv4  31592  mdandyv5  31593  mdandyv6  31594  mdandyv7  31595  mdandyv8  31596  mdandyv9  31597  mdandyv10  31598  mdandyv11  31599  mdandyv12  31600  mdandyv13  31601  mdandyv14  31602  mdandyv15  31603  mdandyvr0  31604  mdandyvr1  31605  mdandyvr2  31606  mdandyvr3  31607  mdandyvr4  31608  mdandyvr5  31609  mdandyvr6  31610  mdandyvr7  31611  mdandyvrx0  31620  mdandyvrx1  31621  mdandyvrx2  31622  mdandyvrx3  31623  mdandyvrx4  31624  mdandyvrx5  31625  mdandyvrx6  31626  mdandyvrx7  31627  dandysum2p2e4  31637  usgra2pthspth  31820  usgra2pthlem1  31822  isfusgracl  31895  isfusgraclALT  31897  usgo0fis  31907  usgo0fisALT  31908  usgresvm1  31912  usgresvm1ALT  31916  sgrp2sgrp  31978  zlmodzxzlmod  32007  zlmodzxzel  32008  zlmodzxzscm  32010  zlmodzxzadd  32011  snlindsntorlem  32144  ldepspr  32147  lmod1lem2  32170  lmod1lem3  32171  lmod1lem4  32172  lmod1lem5  32173  lmodn0  32177  zlmodzxznm  32179  zlmodzxzldeplem  32180  zlmodzxzldeplem1  32182  zlmodzxzldeplem3  32184  lvecpsslmod  32189  ldepsnlinc  32190  ldepslinc  32191  dpfrac1  32247  alimp-surprise  32276  ax6e2nd  32411  uun0.1  32655  relopabVD  32781  ax6e2ndVD  32788  sb5ALTVD  32793  ax6e2ndALT  32810  bj-2upln1upl  33663  bj-vtoclgfALT  33669  ishlatiN  34152  0psubN  34545  atpsubN  34549  taupilem1  36767
  Copyright terms: Public domain W3C validator