MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm3.2i 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  2165  unssi  3482  ssini  3524  bm1.3ii  4293  epelg  4455  elvv  4895  funpr  5461  mpt2v  6122  caovcom  6203  1st2val  6331  2nd2val  6332  elxp7  6338  tfr1a  6614  oeoa  6799  oeoe  6801  erov  6960  th3q  6972  endisj  7154  phplem2  7246  r1funlim  7648  dfac2  7967  cflecard  8089  canth4  8478  canthnumlem  8479  canthwelem  8481  canthp1lem2  8484  pwfseqlem4  8493  wunex3  8572  recexsrlem  8934  mulcani  9617  div1  9663  recdiv  9676  divdiv1  9681  divdiv2  9682  div23i  9728  div11i  9729  divmuldivi  9730  divadddivi  9732  divdivdivi  9733  lemulge11  9828  negiso  9940  dfnn3  9970  1mhlfehlf  10146  halfpm6th  10148  2halves  10152  halfaddsub  10157  avglt1  10161  avglt2  10162  nneo  10309  zeo  10311  x2times  10834  xrsupsslem  10841  xrinfmsslem  10842  injresinjlem  11154  om2uzoi  11250  fzennn  11262  expge1  11372  faclbnd2  11537  faclbnd4lem1  11539  hashf  11580  hashsnlei  11635  hashunlei  11639  hashsslei  11640  f1oun2prg  11819  cjreb  11883  sqr2gt1lt2  12035  abs1m  12094  amgm2  12128  climcndslem2  12585  efcllem  12635  ege2le3  12647  efi4p  12693  efival  12708  cosmul  12729  sin01bnd  12741  cos01bnd  12742  cos1bnd  12743  cos2bnd  12744  cos01gt0  12747  sin02gt0  12748  sincos2sgn  12750  sin4lt0  12751  egt2lt3  12760  rpnnen2lem3  12771  rpnnen2lem11  12779  nthruc  12805  nthruz  12806  odd2np1  12863  divalglem5  12872  ndvdsi  12885  bitsp1o  12900  pythagtriplem12  13155  pythagtriplem14  13157  pythagtriplem15  13158  pythagtriplem16  13159  pythagtriplem17  13160  pcrec  13187  prmrec  13245  modsubi  13363  structfn  13437  strlemor0  13510  strlemor1  13511  strleun  13514  sscres  13978  ga0  15030  0frgp  15366  psrbag0  16509  psrbagsn  16510  cnfld1  16681  cnsubdrglem  16704  expmhm  16731  expghm  16732  isbasis3g  16969  fctop  17023  cctop  17025  bl2in  18383  dscmet  18573  iihalf1  18909  iihalf2  18911  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  minveclem2  19280  minveclem4  19286  ovolunlem1a  19345  volf  19378  i1f1lem  19534  mbfi1fseqlem5  19564  dveflem  19816  pilem2  20321  pilem3  20322  sinhalfpilem  20327  ptolemy  20357  sincosq1lem  20358  sincosq4sgn  20362  tangtx  20366  sinq12gt0  20368  sincos4thpi  20374  sincos6thpi  20376  sincos3rdpi  20377  pige3  20378  coskpi  20381  coseq1  20383  efeq1  20384  efif1olem4  20400  dvsqr  20581  angneg  20598  ang180lem1  20604  ang180lem2  20605  1cubrlem  20634  dquartlem1  20644  quart1  20649  atan1  20721  log2cnv  20737  log2tlbnd  20738  log2ublem1  20739  log2ub  20742  emcllem1  20787  emcllem6  20792  basellem1  20816  basellem2  20817  basellem3  20818  basellem8  20823  ppiublem1  20939  ppiublem2  20940  ppiub  20941  chtublem  20948  chtub  20949  bcmono  21014  bclbnd  21017  bpos1lem  21019  bposlem1  21021  bposlem2  21022  bposlem3  21023  bposlem4  21024  bposlem5  21025  bposlem6  21026  bposlem7  21027  bposlem8  21028  bposlem9  21029  lgsdir2lem1  21060  chebbnd1lem1  21116  chebbnd1lem3  21118  chebbnd1  21119  dchrisum0flblem2  21156  dchrisum0lem1  21163  mulog2sumlem2  21182  selberglem2  21193  chpdifbndlem1  21200  usgraexvlem  21367  usgraexmpldifpr  21372  0trl  21499  2trllemH  21505  2trllemE  21506  2wlklemA  21507  2wlklemB  21508  2wlklemC  21509  wlkntrllem2  21513  wlkntrl  21515  0pth  21523  0pthonv  21534  constr1trl  21541  1pthon  21544  1pthon2v  21546  constr2spth  21553  constr2pth  21554  2pthon  21555  2pthon3v  21557  constr3lem1  21585  constr3lem4  21587  constr3trllem3  21592  constr3pthlem2  21596  ex-natded5.2i  21667  ex-an  21683  ex-id  21695  ex-po  21696  ex-fl  21708  cnrngo  21944  nvz0  22110  ipidsq  22162  ipdirilem  22283  siilem1  22305  minvecolem2  22330  minvecolem3  22331  minvecolem4  22335  hvsubcan  22529  hvsubcan2  22530  normlem7tALT  22574  helch  22699  hsn0elch  22703  hhshsslem2  22721  hhsssh  22722  shscli  22772  shintcli  22784  shintcl  22785  chintcli  22786  chintcl  22787  shincli  22817  shsval2i  22842  omlsi  22859  chincli  22915  chabs1  22971  fh1i  23076  fh2i  23077  cm2ji  23080  pjnormi  23176  nmopsetn0  23321  nmfnsetn0  23334  lnophm  23475  nmcexi  23482  nmbdfnlb  23506  imaelshi  23514  nlelshi  23516  nmopadjlem  23545  nmopcoadji  23557  hmopidmch  23609  hmopidmpj  23610  sto1i  23692  stlei  23696  stji1i  23698  csmdsymi  23790  chirred  23851  cdj3lem1  23890  xrge0iifmhm  24278  cnzh  24307  rezh  24308  qqh0  24321  qqh1  24322  prsiga  24467  coinfliprv  24693  ballotlem1  24697  ballotth  24748  subfacval2  24826  erdszelem2  24831  cvmliftlem4  24928  4bc2eq6  25157  dfpo2  25326  br6  25328  dfon2lem3  25355  poseq  25467  wfrlem13  25482  wfr3  25489  fullfunfnv  25699  axlowdimlem4  25788  axlowdimlem5  25789  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem8  25792  axlowdimlem10  25794  axlowdimlem11  25795  bpoly3  26008  onpsstopbas  26084  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem2  26156  fneref  26254  refref  26255  filnetlem2  26298  filnetlem3  26299  heiborlem6  26415  heiborlem7  26416  riscer  26494  mzpclall  26674  diophin  26721  diophun  26722  eldioph4b  26762  irrapx1  26781  2nn0ind  26898  aomclem4  27022  f1otrspeq  27258  matmulr  27335  lhe4.4ex1a  27414  expgrowth  27420  fnchoice  27567  itgsinexplem1  27615  stoweidlem13  27629  stoweidlem14  27630  stoweidlem24  27640  stoweidlem26  27642  stoweidlem34  27650  stoweidlem49  27665  stoweidlem59  27675  wallispilem4  27684  astbstanbst  27744  aistbistaandb  27745  abnotataxb  27752  mdandyv0  27761  mdandyv1  27762  mdandyv2  27763  mdandyv3  27764  mdandyv4  27765  mdandyv5  27766  mdandyv6  27767  mdandyv7  27768  mdandyv8  27769  mdandyv9  27770  mdandyv10  27771  mdandyv11  27772  mdandyv12  27773  mdandyv13  27774  mdandyv14  27775  mdandyv15  27776  mdandyvr0  27777  mdandyvr1  27778  mdandyvr2  27779  mdandyvr3  27780  mdandyvr4  27781  mdandyvr5  27782  mdandyvr6  27783  mdandyvr7  27784  mdandyvrx0  27793  mdandyvrx1  27794  mdandyvrx2  27795  mdandyvrx3  27796  mdandyvrx4  27797  mdandyvrx5  27798  mdandyvrx6  27799  mdandyvrx7  27800  dandysum2p2e4  27810  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  usgra2adedgspth  28045  usgra2adedgwlk  28046  usgra2adedgwlkon  28047  usg2wlk  28049  usg2wlkon  28050  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  usg2wlkonot  28080  usg2wotspth  28081  frgrancvvdgeq  28146  dpfrac1  28229  a9e2nd  28356  uun0.1  28599  relopabVD  28722  a9e2ndVD  28729  sb5ALTVD  28734  a9e2ndALT  28752  ishlatiN  29838  0psubN  30231  atpsubN  30235
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