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  1166  unssi  3640  ssini  3682  bm1.3ii  4525  epelg  4742  elvv  5006  funpr  5578  mpt2v  6291  caovcom  6371  1st2val  6713  2nd2val  6714  elxp7  6720  tfr1a  6964  oeoa  7147  oeoe  7149  erov  7308  th3q  7320  endisj  7509  phplem2  7602  snopfsupp  7755  cantnffvalOLD  7983  r1funlim  8085  dfac2  8412  cflecard  8534  canth4  8926  canthnumlem  8927  canthwelem  8929  canthp1lem2  8932  pwfseqlem4  8941  wunex3  9020  recexsrlem  9382  mulcani  10087  div1  10135  recdiv  10149  divdiv1  10154  divdiv2  10155  div23i  10201  div11i  10202  divmuldivi  10203  divadddivi  10205  divdivdivi  10206  lemulge11  10303  negiso  10418  dfnn3  10448  2cnne0  10648  2rene0  10649  halfpm6th  10658  avglt1  10674  avglt2  10675  x2times  11374  xrsupsslem  11381  xrinfmsslem  11382  injresinjlem  11756  om2uzoi  11896  fzennn  11908  expge1  12019  faclbnd2  12185  faclbnd4lem1  12187  hashf  12228  hashsnlei  12289  hashunlei  12294  hashsslei  12295  hash2prd  12300  lsw0g  12387  repswccat  12542  cshwsexa  12577  f1oun2prg  12646  wrdlen2i  12665  cjreb  12731  sqr2gt1lt2  12883  abs1m  12942  amgm2  12976  climcndslem2  13432  efcllem  13482  ege2le3  13494  efi4p  13540  efival  13555  sin01bnd  13588  cos01bnd  13589  cos1bnd  13590  cos2bnd  13591  cos01gt0  13594  sin02gt0  13595  sincos2sgn  13597  sin4lt0  13598  egt2lt3  13607  rpnnen2lem3  13618  rpnnen2lem11  13626  nthruc  13652  nthruz  13653  divalglem5  13720  ndvdsi  13733  bitsp1o  13748  pcrec  14044  prmrec  14102  modsubi  14220  structfn  14306  strlemor0  14384  strlemor1  14385  strleun  14388  sscres  14856  ga0  15936  symg2bas  16023  f1otrspeq  16073  psgnsn  16146  0frgp  16398  srgbinomlem4  16765  psrbag0  17701  psrbagsn  17702  coe1mul2  17847  evls1sca  17884  cnfld1  17967  cnsubdrglem  17990  expmhm  18006  expghm  18049  expghmOLD  18050  matmulr  18439  m2detleib  18570  smadiadetglem1  18610  isbasis3g  18687  fctop  18741  cctop  18743  bl2in  20108  dscmet  20298  iihalf1  20636  iihalf2  20638  icopnfhmeo  20648  iccpnfhmeo  20650  xrhmeo  20651  minveclem2  21046  minveclem4  21052  ovolunlem1a  21112  volf  21145  i1f1lem  21301  mbfi1fseqlem5  21331  dveflem  21585  pilem2  22051  pilem3  22052  sinhalfpilem  22059  sincosq1lem  22093  tangtx  22101  sinq12gt0  22103  sincos4thpi  22109  sincos6thpi  22111  sincos3rdpi  22112  pige3  22113  coseq1  22118  efeq1  22119  efif1olem4  22135  angneg  22333  ang180lem1  22339  1cubrlem  22370  quart1  22385  log2cnv  22473  log2tlbnd  22474  log2ublem1  22475  log2ub  22478  emcllem1  22523  emcllem6  22528  basellem1  22552  basellem2  22553  basellem3  22554  basellem8  22559  ppiublem1  22675  ppiublem2  22676  ppiub  22677  chtublem  22684  chtub  22685  bcmono  22750  bclbnd  22753  bpos1lem  22755  bposlem1  22757  bposlem2  22758  bposlem3  22759  bposlem4  22760  bposlem5  22761  bposlem6  22762  bposlem7  22763  bposlem8  22764  bposlem9  22765  lgsdir2lem1  22796  chebbnd1lem1  22852  chebbnd1lem3  22854  chebbnd1  22855  dchrisum0flblem2  22892  dchrisum0lem1  22899  mulog2sumlem2  22918  selberglem2  22929  chpdifbndlem1  22936  ercgrg  23106  axlowdimlem4  23344  axlowdimlem5  23345  axlowdimlem6  23346  axlowdimlem7  23347  axlowdimlem8  23348  axlowdimlem10  23350  axlowdimlem11  23351  usgraexvlem  23466  usgraexmpldifpr  23471  0trl  23598  2trllemH  23604  2trllemE  23605  2wlklemA  23606  2wlklemB  23607  2wlklemC  23608  wlkntrllem2  23612  wlkntrl  23614  0pth  23622  0pthonv  23633  constr1trl  23640  1pthon  23643  1pthon2v  23645  constr2spth  23652  constr2pth  23653  2pthon  23654  2pthon3v  23656  constr3lem1  23684  constr3lem4  23686  constr3trllem3  23691  constr3pthlem2  23695  ex-natded5.2i  23766  ex-an  23782  ex-id  23794  ex-po  23795  ex-fl  23807  cnrngo  24043  nvz0  24209  ipidsq  24261  ipdirilem  24382  siilem1  24404  minvecolem2  24429  minvecolem3  24430  minvecolem4  24434  hvsubcan  24629  hvsubcan2  24630  normlem7tALT  24674  helch  24799  hsn0elch  24804  hhshsslem2  24822  hhsssh  24823  shscli  24873  shintcli  24885  shintcl  24886  chintcli  24887  chintcl  24888  shincli  24918  shsval2i  24943  omlsi  24960  chincli  25016  chabs1  25072  fh1i  25177  fh2i  25178  cm2ji  25181  pjnormi  25277  nmopsetn0  25422  nmfnsetn0  25435  lnophm  25576  nmcexi  25583  nmbdfnlb  25607  imaelshi  25615  nlelshi  25617  nmopadjlem  25646  nmopcoadji  25658  hmopidmch  25710  hmopidmpj  25711  sto1i  25793  stlei  25797  stji1i  25799  csmdsymi  25891  chirred  25952  cdj3lem1  25991  xrsclat  26287  reofld  26454  nn0archi  26457  xrge0iifmhm  26515  cnzh  26545  rezh  26546  qqh0  26559  qqh1  26560  rerrext  26584  cnrrext  26585  prsiga  26720  oms0  26855  coinfliprv  27010  ballotlem1  27014  ballotth  27065  signsw0g  27102  signswmnd  27103  subfacval2  27220  erdszelem2  27225  cvmliftlem4  27322  problem4  27446  quad3  27448  4bc2eq6  27536  dfpo2  27710  br6  27712  dfon2lem3  27743  poseq  27859  wfrlem13  27881  wfr3  27887  fullfunfnv  28122  bpoly3  28346  onpsstopbas  28421  sin2h  28571  cos2h  28572  tan2h  28573  mblfinlem3  28579  mblfinlem4  28580  ismblfin  28581  dvtanlem  28590  itg2addnclem2  28593  asindmre  28628  fneref  28705  refref  28706  filnetlem2  28749  filnetlem3  28750  heiborlem7  28865  riscer  28943  ac6s6f  29134  mzpclall  29212  diophin  29260  diophun  29261  eldioph4b  29299  irrapx1  29318  2nn0ind  29435  aomclem4  29559  lhe4.4ex1a  29752  expgrowth  29758  fnchoice  29900  itgsinexplem1  29943  stoweidlem13  29957  stoweidlem14  29958  stoweidlem26  29970  stoweidlem34  29978  stoweidlem49  29993  stoweidlem59  30003  astbstanbst  30072  aistbistaandb  30073  abnotataxb  30080  mdandyv0  30089  mdandyv1  30090  mdandyv2  30091  mdandyv3  30092  mdandyv4  30093  mdandyv5  30094  mdandyv6  30095  mdandyv7  30096  mdandyv8  30097  mdandyv9  30098  mdandyv10  30099  mdandyv11  30100  mdandyv12  30101  mdandyv13  30102  mdandyv14  30103  mdandyv15  30104  mdandyvr0  30105  mdandyvr1  30106  mdandyvr2  30107  mdandyvr3  30108  mdandyvr4  30109  mdandyvr5  30110  mdandyvr6  30111  mdandyvr7  30112  mdandyvrx0  30121  mdandyvrx1  30122  mdandyvrx2  30123  mdandyvrx3  30124  mdandyvrx4  30125  mdandyvrx5  30126  mdandyvrx6  30127  mdandyvrx7  30128  dandysum2p2e4  30138  hash2prv  30375  wlkcomp  30435  usgra2pthspth  30444  usgra2wlkspthlem1  30445  usgra2wlkspthlem2  30446  usgra2pthlem1  30449  usgra2adedgspth  30454  usgra2adedgwlk  30455  usgra2adedgwlkon  30456  usg2wlk  30458  usg2wlkon  30459  el2wlkonot  30537  el2spthonot  30538  el2spthonot0  30539  usg2wlkonot  30551  usg2wotspth  30552  clwlkcomp  30575  frgrancvvdgeq  30785  numclwwlk1  30840  numclwwlk2lem3  30848  frgraregord013  30860  zlmodzxzlmod  30900  zlmodzxzel  30901  zlmodzxzscm  30903  zlmodzxzadd  30904  gsummptnn0fz  30959  coe1fsupp  30985  mat1dimelbas  31034  snlindsntorlem  31137  ldepspr  31140  lmod1lem2  31163  lmod1lem3  31164  lmod1lem4  31165  lmod1lem5  31166  lmodn0  31170  zlmodzxznm  31172  zlmodzxzldeplem  31173  zlmodzxzldeplem1  31175  zlmodzxzldeplem3  31177  lvecpsslmod  31182  ldepsnlinc  31183  ldepslinc  31184  pmatcollpw3fi1lem2  31275  cpmidpmatlem2  31358  cpmadumatpolylem1  31368  cayhamlem3  31375  cayhamlem4  31376  dpfrac1  31436  alimp-surprise  31465  ax6e2nd  31600  uun0.1  31844  relopabVD  31970  ax6e2ndVD  31977  sb5ALTVD  31982  ax6e2ndALT  31999  bj-2upln1upl  32850  bj-vtoclgfALT  32856  ishlatiN  33339  0psubN  33732  atpsubN  33736  taupilem1  35954
  Copyright terms: Public domain W3C validator