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

Theorem pm3.2i 453
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 445 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
41, 2, 3mp2 9 1  |-  ( ph  /\ 
ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367
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 369
This theorem is referenced by:  pm4.87  582  dfbi  627  mp4an  671  3pm3.2i  1172  unssi  3665  ssini  3707  bm1.3ii  4563  epelg  4781  elvv  5047  funpr  5621  mpt2v  6365  caovcom  6445  1st2val  6799  2nd2val  6800  elxp7  6806  tfr1a  7055  oeoa  7238  oeoe  7240  erov  7400  endisj  7597  phplem2  7690  snopfsupp  7844  cantnffvalOLD  8073  r1funlim  8175  dfac2  8502  cflecard  8624  canth4  9014  canthnumlem  9015  canthwelem  9017  canthp1lem2  9020  pwfseqlem4  9029  wunex3  9108  addsrpr  9441  mulsrpr  9442  recexsrlem  9469  mulcani  10184  div1  10232  recdiv  10246  divdiv1  10251  divdiv2  10252  div23i  10298  div11i  10299  divmuldivi  10300  divadddivi  10302  divdivdivi  10303  lemulge11  10400  negiso  10514  dfnn3  10545  2cnne0  10746  2rene0  10747  halfpm6th  10756  avglt1  10772  avglt2  10773  x2times  11494  xrsupsslem  11501  xrinfmsslem  11502  injresinjlem  11906  om2uzoi  12051  fzennn  12063  expge1  12188  faclbnd2  12354  faclbnd4lem1  12356  hashf  12397  hashsnlei  12465  hashunlei  12470  hashsslei  12471  hash2prd  12505  hash2prv  12512  repswccat  12751  cshwsexa  12786  f1oun2prg  12859  wrdlen2i  12878  relexpaddg  12971  cjreb  13041  sqrt2gt1lt2  13193  abs1m  13253  amgm2  13287  climcndslem2  13747  efcllem  13898  ege2le3  13910  efi4p  13957  efival  13972  sin01bnd  14005  cos01bnd  14006  cos1bnd  14007  cos2bnd  14008  cos01gt0  14011  sin02gt0  14012  sincos2sgn  14014  sin4lt0  14015  egt2lt3  14024  rpnnen2lem3  14037  rpnnen2lem11  14045  nthruc  14071  nthruz  14072  divalglem5  14142  ndvdsi  14155  bitsp1o  14170  pcrec  14469  prmrec  14527  modsubi  14645  structfn  14732  strlemor0  14813  strlemor1  14814  strleun  14817  isofn  15266  sscres  15314  funcestrcsetclem7  15617  funcestrcsetclem8  15618  fullestrcsetc  15622  mgmnsgrpex  16251  ga0  16538  symg2bas  16625  f1otrspeq  16674  psgnsn  16747  0frgp  16999  gsummptnn0fz  17212  srgbinomlem4  17392  psrbag0  18357  psrbagsn  18358  coe1fsupp  18452  coe1mul2  18508  evls1sca  18558  cnfld1  18641  cnsubdrglem  18667  expmhm  18683  expghm  18711  matmulr  19110  mat1dimelbas  19143  mat1f1o  19150  m2detleib  19303  smadiadetglem1  19343  pmatcollpw3fi1lem2  19458  cpmidpmatlem2  19542  cpmadumatpolylem1  19552  cayhamlem3  19558  cayhamlem4  19559  isbasis3g  19620  fctop  19675  cctop  19677  refref  20183  bl2in  21072  dscmet  21262  iihalf1  21600  iihalf2  21602  icopnfhmeo  21612  iccpnfhmeo  21614  xrhmeo  21615  minveclem2  22010  minveclem4  22016  ovolunlem1a  22076  volf  22109  i1f1lem  22265  mbfi1fseqlem5  22295  dveflem  22549  pilem2  23016  pilem3  23017  sinhalfpilem  23025  sincosq1lem  23059  tangtx  23067  sinq12gt0  23069  sincos4thpi  23075  sincos6thpi  23077  sincos3rdpi  23078  pige3  23079  coseq1  23084  efeq1  23085  efif1olem4  23101  logblog  23334  angneg  23337  ang180lem1  23343  1cubrlem  23372  quart1  23387  log2cnv  23475  log2tlbnd  23476  log2ublem1  23477  log2ub  23480  emcllem1  23526  emcllem6  23531  basellem1  23555  basellem2  23556  basellem3  23557  basellem8  23562  ppiublem1  23678  ppiublem2  23679  ppiub  23680  chtublem  23687  chtub  23688  bcmono  23753  bclbnd  23756  bpos1lem  23758  bposlem1  23760  bposlem2  23761  bposlem3  23762  bposlem4  23763  bposlem5  23764  bposlem6  23765  bposlem7  23766  bposlem8  23767  bposlem9  23768  lgsdir2lem1  23799  chebbnd1lem1  23855  chebbnd1lem3  23857  chebbnd1  23858  dchrisum0flblem2  23895  dchrisum0lem1  23902  mulog2sumlem2  23921  selberglem2  23932  chpdifbndlem1  23939  ercgrg  24112  axlowdimlem4  24453  axlowdimlem5  24454  axlowdimlem6  24455  axlowdimlem7  24456  axlowdimlem8  24457  axlowdimlem10  24459  axlowdimlem11  24460  usgraexvlem  24600  usgraexmpldifpr  24605  usgraexmpledg  24608  wlkcomp  24730  0trl  24753  2trllemH  24759  2trllemE  24760  2wlklemA  24761  2wlklemB  24762  2wlklemC  24763  wlkntrllem2  24767  wlkntrl  24769  0pth  24777  0pthonv  24788  constr1trl  24795  1pthon  24798  1pthon2v  24800  constr2spth  24807  constr2pth  24808  2pthon  24809  2pthon3v  24811  usgra2adedgspth  24818  usgra2adedgwlk  24819  usgra2adedgwlkon  24820  usg2wlk  24822  usg2wlkon  24823  usgra2wlkspthlem1  24824  usgra2wlkspthlem2  24825  constr3lem1  24850  constr3lem4  24852  constr3trllem3  24857  constr3pthlem2  24861  clwlkcomp  24968  el2wlkonot  25074  el2spthonot  25075  el2spthonot0  25076  usg2wlkonot  25088  usg2wotspth  25089  frgrancvvdgeq  25248  numclwwlk1  25303  numclwwlk2lem3  25311  frgraregord013  25323  ex-natded5.2i  25332  ex-an  25348  ex-id  25360  ex-po  25361  ex-fl  25373  cnrngo  25606  nvz0  25772  ipidsq  25824  ipdirilem  25945  siilem1  25967  minvecolem2  25992  minvecolem3  25993  minvecolem4  25997  hvsubcan  26192  hvsubcan2  26193  normlem7tALT  26237  helch  26362  hsn0elch  26367  hhshsslem2  26385  hhsssh  26386  shscli  26436  shintcli  26448  shintcl  26449  chintcli  26450  chintcl  26451  shincli  26481  shsval2i  26506  omlsi  26523  chincli  26579  chabs1  26635  fh1i  26740  fh2i  26741  cm2ji  26744  pjnormi  26840  nmopsetn0  26985  nmfnsetn0  26998  lnophm  27139  nmcexi  27146  nmbdfnlb  27170  imaelshi  27178  nlelshi  27180  nmopadjlem  27209  nmopcoadji  27221  hmopidmch  27273  hmopidmpj  27274  sto1i  27356  stlei  27360  stji1i  27362  csmdsymi  27454  chirred  27515  cdj3lem1  27554  xrsclat  27905  nn0archi  28071  xrge0iifmhm  28159  qqh0  28202  qqh1  28203  rerrext  28227  cnrrext  28228  prsiga  28364  oms0  28508  coinfliprv  28688  ballotlem1  28692  ballotth  28743  signsw0g  28780  subfacval2  28898  erdszelem2  28903  cvmliftlem4  29000  elmrsubrn  29147  msubfval  29151  problem4  29289  quad3  29291  4bc2eq6  29356  dfpo2  29428  br6  29430  dfon2lem3  29460  poseq  29576  wfrlem13  29598  wfr3  29604  fullfunfnv  29827  bpoly3  30051  onpsstopbas  30126  sin2h  30288  cos2h  30289  tan2h  30290  mblfinlem3  30296  mblfinlem4  30297  ismblfin  30298  dvtanlem  30307  itg2addnclem2  30310  asindmre  30345  fneref  30411  filnetlem2  30440  filnetlem3  30441  heiborlem7  30556  riscer  30634  ac6s6f  30824  mzpclall  30902  diophin  30948  diophun  30949  eldioph4b  30987  irrapx1  31006  2nn0ind  31123  aomclem4  31245  lhe4.4ex1a  31478  expgrowth  31484  fnchoice  31647  fprodn0f  31836  dvmptconst  31952  dvmptidg  31954  dvmulcncf  31964  dvdivcncf  31966  dvnprodlem3  31987  itgsinexplem1  31994  stoweidlem13  32037  stoweidlem14  32038  stoweidlem26  32050  stoweidlem34  32058  stoweidlem49  32073  stoweidlem59  32083  dirkertrigeqlem3  32124  dirkercncflem1  32127  dirkercncflem2  32128  fourierdlem57  32188  fourierdlem62  32193  fourierdlem103  32234  fourierdlem111  32242  fourierswlem  32255  fouriersw  32256  astbstanbst  32346  aistbistaandb  32347  abnotataxb  32354  mdandyv0  32363  mdandyv1  32364  mdandyv2  32365  mdandyv3  32366  mdandyv4  32367  mdandyv5  32368  mdandyv6  32369  mdandyv7  32370  mdandyv8  32371  mdandyv9  32372  mdandyv10  32373  mdandyv11  32374  mdandyv12  32375  mdandyv13  32376  mdandyv14  32377  mdandyv15  32378  mdandyvr0  32379  mdandyvr1  32380  mdandyvr2  32381  mdandyvr3  32382  mdandyvr4  32383  mdandyvr5  32384  mdandyvr6  32385  mdandyvr7  32386  mdandyvrx0  32395  mdandyvrx1  32396  mdandyvrx2  32397  mdandyvrx3  32398  mdandyvrx4  32399  mdandyvrx5  32400  mdandyvrx6  32401  mdandyvrx7  32402  dandysum2p2e4  32412  mod2eq1n2dvds  32537  zofldiv2ALTV  32576  41prothprmlem2  32624  pfx2  32659  usgra2pthspth  32742  usgra2pthlem1  32744  isfusgracl  32817  isfusgraclALT  32819  usgo0fis  32829  usgo0fisALT  32830  usgresvm1  32834  usgresvm1ALT  32838  mgmplusgiopALT  32909  sgrp2sgrp  32943  isrnghm  32971  2zrngaabl  33023  rnghmsscmap2  33054  rnghmsscmap  33055  funcrngcsetc  33079  funcrngcsetcALT  33080  rhmsscmap2  33100  rhmsscmap  33101  funcringcsetc  33116  funcringcsetcALTV2lem8  33124  funcringcsetclem8ALTV  33147  zlmodzxzlmod  33216  zlmodzxzel  33217  zlmodzxzscm  33219  zlmodzxzadd  33220  snlindsntorlem  33344  ldepspr  33347  lmod1lem2  33362  lmod1lem3  33363  lmod1lem4  33364  lmod1lem5  33365  lmodn0  33369  zlmodzxznm  33371  zlmodzxzldeplem  33372  zlmodzxzldeplem1  33374  zlmodzxzldeplem3  33376  lvecpsslmod  33381  ldepsnlinc  33382  ldepslinc  33383  divlt1lt  33391  expnegico01  33396  3halfnz  33399  nno  33411  zofldiv2  33421  flnn0div2ge  33423  elbigo2  33446  nnlog2ge0lt1  33460  digfval  33491  dignnld  33497  dignn0flhalf  33512  dpfrac1  33575  alimp-surprise  33602  aacllem  33623  ax6e2nd  33744  uun0.1  33988  relopabVD  34121  ax6e2ndVD  34128  sb5ALTVD  34133  ax6e2ndALT  34150  bj-2upln1upl  35002  bj-vtoclgfALT  35008  ishlatiN  35496  0psubN  35889  atpsubN  35893  taupilem1  38112  ifpbi1b  38123  ifpid2g  38126  ifpid3g  38127  pwinfi  38181  dfrcl2  38214  relexp0idm  38241  relexp1idm  38242
  Copyright terms: Public domain W3C validator