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

Theorem pm3.2i 441
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 434 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 17 1  |-  ( ph  /\ 
ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 358
This theorem is referenced by:  pm4.87  567  dfbi  610  mp4an  654  3pm3.2i  1130  pm11.07  2067  unssi  3363  ssini  3405  bm1.3ii  4160  epelg  4322  elvv  4764  funpr  5318  mpt2v  5953  caovcom  6033  1st2val  6161  2nd2val  6162  elxp7  6168  tfr1a  6426  oeoa  6611  oeoe  6613  erov  6771  th3q  6783  endisj  6965  phplem2  7057  r1funlim  7454  dfac2  7773  cflecard  7895  canth4  8285  canthnumlem  8286  canthwelem  8288  canthp1lem2  8291  pwfseqlem4  8300  wunex3  8379  recexsrlem  8741  mulcani  9423  div1  9469  recdiv  9482  divdiv1  9487  divdiv2  9488  div23i  9534  div11i  9535  divmuldivi  9536  divadddivi  9538  divdivdivi  9539  lemulge11  9634  negiso  9746  dfnn3  9776  1mhlfehlf  9950  halfpm6th  9952  2halves  9956  halfaddsub  9961  avglt1  9965  avglt2  9966  nneo  10111  zeo  10113  x2times  10635  xrsupsslem  10641  xrinfmsslem  10642  om2uzoi  11034  fzennn  11046  expge1  11155  faclbnd2  11320  faclbnd4lem1  11322  hashf  11360  hashsnlei  11392  hashunlei  11393  hashsslei  11394  cjreb  11624  sqr2gt1lt2  11776  abs1m  11835  amgm2  11869  climcndslem2  12325  efcllem  12375  ege2le3  12387  efi4p  12433  efival  12448  cosmul  12469  sin01bnd  12481  cos01bnd  12482  cos1bnd  12483  cos2bnd  12484  cos01gt0  12487  sin02gt0  12488  sincos2sgn  12490  sin4lt0  12491  egt2lt3  12500  rpnnen2lem3  12511  rpnnen2lem11  12519  nthruc  12545  nthruz  12546  odd2np1  12603  divalglem5  12612  ndvdsi  12625  bitsp1o  12640  pythagtriplem12  12895  pythagtriplem14  12897  pythagtriplem15  12898  pythagtriplem16  12899  pythagtriplem17  12900  pcrec  12927  prmrec  12985  modsubi  13103  structfn  13177  strlemor0  13250  strlemor1  13251  strleun  13254  sscres  13716  ga0  14768  0frgp  15104  psrbag0  16251  psrbagsn  16252  cnfld1  16415  cnsubdrglem  16438  expmhm  16465  expghm  16466  isbasis3g  16703  fctop  16757  cctop  16759  bl2in  17973  dscmet  18111  iihalf1  18445  iihalf2  18447  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  minveclem2  18806  minveclem4  18812  ovolunlem1a  18871  volf  18904  i1f1lem  19060  mbfi1fseqlem5  19090  dveflem  19342  pilem2  19844  pilem3  19845  sinhalfpilem  19850  ptolemy  19880  sincosq1lem  19881  sincosq4sgn  19885  tangtx  19889  sinq12gt0  19891  sincos4thpi  19897  sincos6thpi  19899  sincos3rdpi  19900  pige3  19901  coskpi  19904  coseq1  19906  efeq1  19907  efif1olem4  19923  dvsqr  20100  angneg  20117  ang180lem1  20123  ang180lem2  20124  1cubrlem  20153  dquartlem1  20163  quart1  20168  atan1  20240  log2cnv  20256  log2tlbnd  20257  log2ublem1  20258  log2ub  20261  emcllem1  20305  emcllem6  20310  basellem1  20334  basellem2  20335  basellem3  20336  basellem8  20341  ppiublem1  20457  ppiublem2  20458  ppiub  20459  chtublem  20466  chtub  20467  bcmono  20532  bclbnd  20535  bpos1lem  20537  bposlem1  20539  bposlem2  20540  bposlem3  20541  bposlem4  20542  bposlem5  20543  bposlem6  20544  bposlem7  20545  bposlem8  20546  bposlem9  20547  lgsdir2lem1  20578  chebbnd1lem1  20634  chebbnd1lem3  20636  chebbnd1  20637  dchrisum0flblem2  20674  dchrisum0lem1  20681  mulog2sumlem2  20700  selberglem2  20711  chpdifbndlem1  20718  ex-natded5.2i  20809  ex-an  20825  ex-id  20837  ex-po  20838  ex-fl  20850  cnrngo  21086  nvz0  21250  ipidsq  21302  ipdirilem  21423  siilem1  21445  minvecolem2  21470  minvecolem3  21471  minvecolem4  21475  hvsubcan  21669  hvsubcan2  21670  normlem7tALT  21714  helch  21839  hsn0elch  21843  hhshsslem2  21861  hhsssh  21862  shscli  21912  shintcli  21924  shintcl  21925  chintcli  21926  chintcl  21927  shincli  21957  shsval2i  21982  omlsi  21999  chincli  22055  chabs1  22111  fh1i  22216  fh2i  22217  cm2ji  22220  pjnormi  22316  nmopsetn0  22461  nmfnsetn0  22474  lnophm  22615  nmcexi  22622  nmbdfnlb  22646  imaelshi  22654  nlelshi  22656  nmopadjlem  22685  nmopcoadji  22697  hmopidmch  22749  hmopidmpj  22750  sto1i  22832  stlei  22836  stji1i  22838  csmdsymi  22930  chirred  22991  cdj3lem1  23030  rinvf1o  23054  ballotlem1  23061  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemimin  23080  ballotlemsdom  23086  ballotlemsel1i  23087  ballotlemsima  23090  ballotlemfrceq  23103  ballotlemfrcn0  23104  ballotth  23112  tpr2rico  23311  xrge0iifmhm  23336  dmvlsiga  23505  prsiga  23507  measbase  23543  ismeas  23545  coinfliprv  23698  coinflippvt  23700  subfacval2  23733  erdszelem2  23738  cvmliftlem4  23834  4bc2eq6  24114  dfpo2  24183  br6  24185  dfon2lem3  24212  poseq  24324  wfrlem13  24339  wfr3  24346  fullfunfnv  24556  axlowdimlem4  24645  axlowdimlem5  24646  axlowdimlem6  24647  axlowdimlem7  24648  axlowdimlem8  24649  axlowdimlem10  24651  axlowdimlem11  24652  bpoly3  24865  onpsstopbas  24941  itg2addnclem2  25004  imfstnrelc  25184  repcpwti  25264  toplat  25393  intopcoaconb  25643  cntrset  25705  mslb1  25710  msra3  25712  claddrv  25750  sigadd  25752  addassv  25759  issubrv  25775  subclrvd  25777  clsmulcv  25785  clsmulrv  25786  fnmulcv  25787  1ded  25841  0ded  25860  0catOLD  25861  1cat  25862  dualalg  25885  catsbc  25952  cmpidmor3  26073  setiscat  26082  fnckle  26148  pfsubkl  26150  pgapspf  26155  pgapspf2  26156  linevala2  26181  pdiveql  26271  fneref  26387  refref  26388  filnetlem2  26431  filnetlem3  26432  heiborlem6  26643  heiborlem7  26644  riscer  26722  mzpclall  26908  diophin  26955  diophun  26956  ftp  26996  eldioph4b  26997  irrapx1  27016  2nn0ind  27133  aomclem4  27257  f1otrspeq  27493  matmulr  27570  lhe4.4ex1a  27649  expgrowth  27655  fnchoice  27803  infrglb  27825  dvcosre  27844  itgsin0pilem1  27847  itgsinexplem1  27851  itgsinexp  27852  stoweidlem5  27857  stoweidlem7  27859  stoweidlem13  27865  stoweidlem14  27866  stoweidlem24  27876  stoweidlem26  27878  stoweidlem28  27880  stoweidlem34  27886  stoweidlem44  27896  stoweidlem49  27901  stoweidlem59  27911  stoweid  27915  wallispilem2  27918  wallispilem3  27919  wallispilem4  27920  wallispi  27922  wallispi2lem1  27923  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem13  27938  stirlinglem15  27940  bothtbothsame  27970  bothfbothsame  27971  aiffbbtat  27972  aisbbisfaisf  27973  aibnbna  27977  aiffbtbat  27979  astbstanbst  27980  aistbistaandb  27981  abnotbtaxb  27987  abnotataxb  27988  mdandyv0  27997  mdandyv1  27998  mdandyv2  27999  mdandyv3  28000  mdandyv4  28001  mdandyv5  28002  mdandyv6  28003  mdandyv7  28004  mdandyv8  28005  mdandyv9  28006  mdandyv10  28007  mdandyv11  28008  mdandyv12  28009  mdandyv13  28010  mdandyv14  28011  mdandyv15  28012  mdandyvr0  28013  mdandyvr1  28014  mdandyvr2  28015  mdandyvr3  28016  mdandyvr4  28017  mdandyvr5  28018  mdandyvr6  28019  mdandyvr7  28020  mdandyvr8  28021  mdandyvr9  28022  mdandyvr10  28023  mdandyvr11  28024  mdandyvr12  28025  mdandyvr13  28026  mdandyvr14  28027  mdandyvr15  28028  mdandyvrx0  28029  mdandyvrx1  28030  mdandyvrx2  28031  mdandyvrx3  28032  mdandyvrx4  28033  mdandyvrx5  28034  mdandyvrx6  28035  mdandyvrx7  28036  mdandyvrx8  28037  mdandyvrx9  28038  mdandyvrx10  28039  mdandyvrx11  28040  mdandyvrx12  28041  mdandyvrx13  28042  mdandyvrx14  28043  mdandyvrx15  28044  dandysum2p2e4  28046  f1oun2prg  28187  injresinjlem  28214  usgraexvlem  28261  usgraexmpldifpr  28266  0trl  28344  wlkntrl  28350  0pth  28356  constr3lem1  28391  constr3lem4  28393  constr3trllem3  28398  constr3pthlem2  28402  dpfrac1  28496  a9e2nd  28623  uun0.1  28867  relopabVD  28993  a9e2ndVD  29000  sb5ALTVD  29005  a9e2ndALT  29023  pm11.07OLD7  29716  ishlatiN  30167  0psubN  30560  atpsubN  30564
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 177  df-an 360
  Copyright terms: Public domain W3C validator