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

Theorem pm3.2i 442
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 435 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 9 1  |-  ( ph  /\ 
ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 359
This theorem is referenced by:  pm4.87  568  dfbi  611  mp4an  655  3pm3.2i  1132  pm11.07OLD  2191  unssi  3514  ssini  3556  bm1.3ii  4325  epelg  4487  elvv  4928  funpr  5494  mpt2v  6155  caovcom  6236  1st2val  6364  2nd2val  6365  elxp7  6371  tfr1a  6647  oeoa  6832  oeoe  6834  erov  6993  th3q  7005  endisj  7187  phplem2  7279  r1funlim  7684  dfac2  8003  cflecard  8125  canth4  8514  canthnumlem  8515  canthwelem  8517  canthp1lem2  8520  pwfseqlem4  8529  wunex3  8608  recexsrlem  8970  mulcani  9653  div1  9699  recdiv  9712  divdiv1  9717  divdiv2  9718  div23i  9764  div11i  9765  divmuldivi  9766  divadddivi  9768  divdivdivi  9769  lemulge11  9864  negiso  9976  dfnn3  10006  1mhlfehlf  10182  halfpm6th  10184  2halves  10188  halfaddsub  10193  avglt1  10197  avglt2  10198  nneo  10345  zeo  10347  x2times  10870  xrsupsslem  10877  xrinfmsslem  10878  injresinjlem  11191  om2uzoi  11287  fzennn  11299  expge1  11409  faclbnd2  11574  faclbnd4lem1  11576  hashf  11617  hashsnlei  11672  hashunlei  11676  hashsslei  11677  f1oun2prg  11856  cjreb  11920  sqr2gt1lt2  12072  abs1m  12131  amgm2  12165  climcndslem2  12622  efcllem  12672  ege2le3  12684  efi4p  12730  efival  12745  cosmul  12766  sin01bnd  12778  cos01bnd  12779  cos1bnd  12780  cos2bnd  12781  cos01gt0  12784  sin02gt0  12785  sincos2sgn  12787  sin4lt0  12788  egt2lt3  12797  rpnnen2lem3  12808  rpnnen2lem11  12816  nthruc  12842  nthruz  12843  odd2np1  12900  divalglem5  12909  ndvdsi  12922  bitsp1o  12937  pythagtriplem12  13192  pythagtriplem14  13194  pythagtriplem15  13195  pythagtriplem16  13196  pythagtriplem17  13197  pcrec  13224  prmrec  13282  modsubi  13400  structfn  13474  strlemor0  13547  strlemor1  13548  strleun  13551  sscres  14015  ga0  15067  0frgp  15403  psrbag0  16546  psrbagsn  16547  cnfld1  16718  cnsubdrglem  16741  expmhm  16768  expghm  16769  isbasis3g  17006  fctop  17060  cctop  17062  bl2in  18422  dscmet  18612  iihalf1  18948  iihalf2  18950  icopnfhmeo  18960  iccpnfhmeo  18962  xrhmeo  18963  minveclem2  19319  minveclem4  19325  ovolunlem1a  19384  volf  19417  i1f1lem  19573  mbfi1fseqlem5  19603  dveflem  19855  pilem2  20360  pilem3  20361  sinhalfpilem  20366  ptolemy  20396  sincosq1lem  20397  sincosq4sgn  20401  tangtx  20405  sinq12gt0  20407  sincos4thpi  20413  sincos6thpi  20415  sincos3rdpi  20416  pige3  20417  coskpi  20420  coseq1  20422  efeq1  20423  efif1olem4  20439  dvsqr  20620  angneg  20637  ang180lem1  20643  ang180lem2  20644  1cubrlem  20673  dquartlem1  20683  quart1  20688  atan1  20760  log2cnv  20776  log2tlbnd  20777  log2ublem1  20778  log2ub  20781  emcllem1  20826  emcllem6  20831  basellem1  20855  basellem2  20856  basellem3  20857  basellem8  20862  ppiublem1  20978  ppiublem2  20979  ppiub  20980  chtublem  20987  chtub  20988  bcmono  21053  bclbnd  21056  bpos1lem  21058  bposlem1  21060  bposlem2  21061  bposlem3  21062  bposlem4  21063  bposlem5  21064  bposlem6  21065  bposlem7  21066  bposlem8  21067  bposlem9  21068  lgsdir2lem1  21099  chebbnd1lem1  21155  chebbnd1lem3  21157  chebbnd1  21158  dchrisum0flblem2  21195  dchrisum0lem1  21202  mulog2sumlem2  21221  selberglem2  21232  chpdifbndlem1  21239  usgraexvlem  21406  usgraexmpldifpr  21411  0trl  21538  2trllemH  21544  2trllemE  21545  2wlklemA  21546  2wlklemB  21547  2wlklemC  21548  wlkntrllem2  21552  wlkntrl  21554  0pth  21562  0pthonv  21573  constr1trl  21580  1pthon  21583  1pthon2v  21585  constr2spth  21592  constr2pth  21593  2pthon  21594  2pthon3v  21596  constr3lem1  21624  constr3lem4  21626  constr3trllem3  21631  constr3pthlem2  21635  ex-natded5.2i  21706  ex-an  21722  ex-id  21734  ex-po  21735  ex-fl  21747  cnrngo  21983  nvz0  22149  ipidsq  22201  ipdirilem  22322  siilem1  22344  minvecolem2  22369  minvecolem3  22370  minvecolem4  22374  hvsubcan  22568  hvsubcan2  22569  normlem7tALT  22613  helch  22738  hsn0elch  22742  hhshsslem2  22760  hhsssh  22761  shscli  22811  shintcli  22823  shintcl  22824  chintcli  22825  chintcl  22826  shincli  22856  shsval2i  22881  omlsi  22898  chincli  22954  chabs1  23010  fh1i  23115  fh2i  23116  cm2ji  23119  pjnormi  23215  nmopsetn0  23360  nmfnsetn0  23373  lnophm  23514  nmcexi  23521  nmbdfnlb  23545  imaelshi  23553  nlelshi  23555  nmopadjlem  23584  nmopcoadji  23596  hmopidmch  23648  hmopidmpj  23649  sto1i  23731  stlei  23735  stji1i  23737  csmdsymi  23829  chirred  23890  cdj3lem1  23929  xrge0iifmhm  24317  cnzh  24346  rezh  24347  qqh0  24360  qqh1  24361  prsiga  24506  coinfliprv  24732  ballotlem1  24736  ballotth  24787  subfacval2  24865  erdszelem2  24870  cvmliftlem4  24967  4bc2eq6  25196  dfpo2  25370  br6  25372  dfon2lem3  25404  poseq  25520  wfrlem13  25542  wfr3  25548  fullfunfnv  25783  axlowdimlem4  25876  axlowdimlem5  25877  axlowdimlem6  25878  axlowdimlem7  25879  axlowdimlem8  25880  axlowdimlem10  25882  axlowdimlem11  25883  bpoly3  26096  onpsstopbas  26172  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  itg2addnclem2  26247  fneref  26355  refref  26356  filnetlem2  26399  filnetlem3  26400  heiborlem6  26516  heiborlem7  26517  riscer  26595  mzpclall  26775  diophin  26822  diophun  26823  eldioph4b  26863  irrapx1  26882  2nn0ind  26999  aomclem4  27123  f1otrspeq  27358  matmulr  27435  lhe4.4ex1a  27514  expgrowth  27520  fnchoice  27667  itgsinexplem1  27715  stoweidlem13  27729  stoweidlem14  27730  stoweidlem24  27740  stoweidlem26  27742  stoweidlem34  27750  stoweidlem49  27765  stoweidlem59  27775  wallispilem4  27784  astbstanbst  27844  aistbistaandb  27845  abnotataxb  27852  mdandyv0  27861  mdandyv1  27862  mdandyv2  27863  mdandyv3  27864  mdandyv4  27865  mdandyv5  27866  mdandyv6  27867  mdandyv7  27868  mdandyv8  27869  mdandyv9  27870  mdandyv10  27871  mdandyv11  27872  mdandyv12  27873  mdandyv13  27874  mdandyv14  27875  mdandyv15  27876  mdandyvr0  27877  mdandyvr1  27878  mdandyvr2  27879  mdandyvr3  27880  mdandyvr4  27881  mdandyvr5  27882  mdandyvr6  27883  mdandyvr7  27884  mdandyvrx0  27893  mdandyvrx1  27894  mdandyvrx2  27895  mdandyvrx3  27896  mdandyvrx4  27897  mdandyvrx5  27898  mdandyvrx6  27899  mdandyvrx7  27900  dandysum2p2e4  27910  cshwsexa  28254  usgra2pthspth  28258  usgra2wlkspthlem1  28259  usgra2wlkspthlem2  28260  usgra2pthlem1  28263  usgra2adedgspth  28268  usgra2adedgwlk  28269  usgra2adedgwlkon  28270  usg2wlk  28272  usg2wlkon  28273  el2wlkonot  28289  el2spthonot  28290  el2spthonot0  28291  usg2wlkonot  28303  usg2wotspth  28304  frgrancvvdgeq  28369  dpfrac1  28452  a9e2nd  28582  uun0.1  28827  relopabVD  28950  a9e2ndVD  28957  sb5ALTVD  28962  a9e2ndALT  28979  ishlatiN  30090  0psubN  30483  atpsubN  30487
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator