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  1173  unssi  3661  ssini  3703  bm1.3ii  4557  epelg  4778  elvv  5044  funpr  5625  mpt2v  6373  caovcom  6453  1st2val  6807  2nd2val  6808  elxp7  6814  tfr1a  7061  oeoa  7244  oeoe  7246  erov  7406  endisj  7602  phplem2  7695  snopfsupp  7850  cantnffvalOLD  8080  r1funlim  8182  dfac2  8509  cflecard  8631  canth4  9023  canthnumlem  9024  canthwelem  9026  canthp1lem2  9029  pwfseqlem4  9038  wunex3  9117  addsrpr  9450  mulsrpr  9451  recexsrlem  9478  mulcani  10189  div1  10237  recdiv  10251  divdiv1  10256  divdiv2  10257  div23i  10303  div11i  10304  divmuldivi  10305  divadddivi  10307  divdivdivi  10308  lemulge11  10405  negiso  10520  dfnn3  10551  2cnne0  10751  2rene0  10752  halfpm6th  10761  avglt1  10777  avglt2  10778  x2times  11495  xrsupsslem  11502  xrinfmsslem  11503  injresinjlem  11899  om2uzoi  12040  fzennn  12052  expge1  12177  faclbnd2  12343  faclbnd4lem1  12345  hashf  12386  hashsnlei  12452  hashunlei  12457  hashsslei  12458  hash2prd  12492  hash2prv  12499  repswccat  12731  cshwsexa  12766  f1oun2prg  12839  wrdlen2i  12858  cjreb  12930  sqrt2gt1lt2  13082  abs1m  13142  amgm2  13176  climcndslem2  13636  efcllem  13686  ege2le3  13698  efi4p  13744  efival  13759  sin01bnd  13792  cos01bnd  13793  cos1bnd  13794  cos2bnd  13795  cos01gt0  13798  sin02gt0  13799  sincos2sgn  13801  sin4lt0  13802  egt2lt3  13811  rpnnen2lem3  13822  rpnnen2lem11  13830  nthruc  13856  nthruz  13857  divalglem5  13927  ndvdsi  13940  bitsp1o  13955  pcrec  14254  prmrec  14312  modsubi  14430  structfn  14517  strlemor0  14595  strlemor1  14596  strleun  14599  sscres  15064  mgmnsgrpex  15918  ga0  16205  symg2bas  16292  f1otrspeq  16341  psgnsn  16414  0frgp  16666  gsummptnn0fz  16883  srgbinomlem4  17062  psrbag0  18027  psrbagsn  18028  coe1fsupp  18122  coe1mul2  18178  evls1sca  18228  cnfld1  18311  cnsubdrglem  18337  expmhm  18353  expghm  18396  expghmOLD  18397  matmulr  18807  mat1dimelbas  18840  mat1f1o  18847  m2detleib  19000  smadiadetglem1  19040  pmatcollpw3fi1lem2  19155  cpmidpmatlem2  19239  cpmadumatpolylem1  19249  cayhamlem3  19255  cayhamlem4  19256  isbasis3g  19317  fctop  19371  cctop  19373  refref  19880  bl2in  20769  dscmet  20959  iihalf1  21297  iihalf2  21299  icopnfhmeo  21309  iccpnfhmeo  21311  xrhmeo  21312  minveclem2  21707  minveclem4  21713  ovolunlem1a  21773  volf  21806  i1f1lem  21962  mbfi1fseqlem5  21992  dveflem  22246  pilem2  22712  pilem3  22713  sinhalfpilem  22721  sincosq1lem  22755  tangtx  22763  sinq12gt0  22765  sincos4thpi  22771  sincos6thpi  22773  sincos3rdpi  22774  pige3  22775  coseq1  22780  efeq1  22781  efif1olem4  22797  angneg  23000  ang180lem1  23006  1cubrlem  23037  quart1  23052  log2cnv  23140  log2tlbnd  23141  log2ublem1  23142  log2ub  23145  emcllem1  23190  emcllem6  23195  basellem1  23219  basellem2  23220  basellem3  23221  basellem8  23226  ppiublem1  23342  ppiublem2  23343  ppiub  23344  chtublem  23351  chtub  23352  bcmono  23417  bclbnd  23420  bpos1lem  23422  bposlem1  23424  bposlem2  23425  bposlem3  23426  bposlem4  23427  bposlem5  23428  bposlem6  23429  bposlem7  23430  bposlem8  23431  bposlem9  23432  lgsdir2lem1  23463  chebbnd1lem1  23519  chebbnd1lem3  23521  chebbnd1  23522  dchrisum0flblem2  23559  dchrisum0lem1  23566  mulog2sumlem2  23585  selberglem2  23596  chpdifbndlem1  23603  ercgrg  23773  axlowdimlem4  24113  axlowdimlem5  24114  axlowdimlem6  24115  axlowdimlem7  24116  axlowdimlem8  24117  axlowdimlem10  24119  axlowdimlem11  24120  usgraexvlem  24260  usgraexmpldifpr  24265  usgraexmpledg  24268  wlkcomp  24390  0trl  24413  2trllemH  24419  2trllemE  24420  2wlklemA  24421  2wlklemB  24422  2wlklemC  24423  wlkntrllem2  24427  wlkntrl  24429  0pth  24437  0pthonv  24448  constr1trl  24455  1pthon  24458  1pthon2v  24460  constr2spth  24467  constr2pth  24468  2pthon  24469  2pthon3v  24471  usgra2adedgspth  24478  usgra2adedgwlk  24479  usgra2adedgwlkon  24480  usg2wlk  24482  usg2wlkon  24483  usgra2wlkspthlem1  24484  usgra2wlkspthlem2  24485  constr3lem1  24510  constr3lem4  24512  constr3trllem3  24517  constr3pthlem2  24521  clwlkcomp  24628  el2wlkonot  24734  el2spthonot  24735  el2spthonot0  24736  usg2wlkonot  24748  usg2wotspth  24749  frgrancvvdgeq  24908  numclwwlk1  24963  numclwwlk2lem3  24971  frgraregord013  24983  ex-natded5.2i  24992  ex-an  25008  ex-id  25020  ex-po  25021  ex-fl  25033  cnrngo  25270  nvz0  25436  ipidsq  25488  ipdirilem  25609  siilem1  25631  minvecolem2  25656  minvecolem3  25657  minvecolem4  25661  hvsubcan  25856  hvsubcan2  25857  normlem7tALT  25901  helch  26026  hsn0elch  26031  hhshsslem2  26049  hhsssh  26050  shscli  26100  shintcli  26112  shintcl  26113  chintcli  26114  chintcl  26115  shincli  26145  shsval2i  26170  omlsi  26187  chincli  26243  chabs1  26299  fh1i  26404  fh2i  26405  cm2ji  26408  pjnormi  26504  nmopsetn0  26649  nmfnsetn0  26662  lnophm  26803  nmcexi  26810  nmbdfnlb  26834  imaelshi  26842  nlelshi  26844  nmopadjlem  26873  nmopcoadji  26885  hmopidmch  26937  hmopidmpj  26938  sto1i  27020  stlei  27024  stji1i  27026  csmdsymi  27118  chirred  27179  cdj3lem1  27218  xrsclat  27534  nn0archi  27699  xrge0iifmhm  27787  qqh0  27831  qqh1  27832  rerrext  27856  cnrrext  27857  prsiga  27997  oms0  28132  coinfliprv  28287  ballotlem1  28291  ballotth  28342  signsw0g  28379  subfacval2  28497  erdszelem2  28502  cvmliftlem4  28599  elmrsubrn  28746  msubfval  28750  problem4  28888  quad3  28890  4bc2eq6  28978  dfpo2  29152  br6  29154  dfon2lem3  29185  poseq  29301  wfrlem13  29323  wfr3  29329  fullfunfnv  29564  bpoly3  29788  onpsstopbas  29863  sin2h  30013  cos2h  30014  tan2h  30015  mblfinlem3  30021  mblfinlem4  30022  ismblfin  30023  dvtanlem  30032  itg2addnclem2  30035  asindmre  30070  fneref  30136  filnetlem2  30165  filnetlem3  30166  heiborlem7  30281  riscer  30359  ac6s6f  30549  mzpclall  30627  diophin  30674  diophun  30675  eldioph4b  30713  irrapx1  30732  2nn0ind  30849  aomclem4  30971  lhe4.4ex1a  31203  expgrowth  31209  fnchoice  31351  dvmptconst  31610  dvmptidg  31612  dvmulcncf  31622  dvdivcncf  31624  itgsinexplem1  31638  stoweidlem13  31680  stoweidlem14  31681  stoweidlem26  31693  stoweidlem34  31701  stoweidlem49  31716  stoweidlem59  31726  dirkertrigeqlem3  31767  dirkercncflem1  31770  dirkercncflem2  31771  fourierdlem57  31831  fourierdlem62  31836  fourierdlem103  31877  fourierdlem111  31885  fourierswlem  31898  fouriersw  31899  astbstanbst  31938  aistbistaandb  31939  abnotataxb  31946  mdandyv0  31955  mdandyv1  31956  mdandyv2  31957  mdandyv3  31958  mdandyv4  31959  mdandyv5  31960  mdandyv6  31961  mdandyv7  31962  mdandyv8  31963  mdandyv9  31964  mdandyv10  31965  mdandyv11  31966  mdandyv12  31967  mdandyv13  31968  mdandyv14  31969  mdandyv15  31970  mdandyvr0  31971  mdandyvr1  31972  mdandyvr2  31973  mdandyvr3  31974  mdandyvr4  31975  mdandyvr5  31976  mdandyvr6  31977  mdandyvr7  31978  mdandyvrx0  31987  mdandyvrx1  31988  mdandyvrx2  31989  mdandyvrx3  31990  mdandyvrx4  31991  mdandyvrx5  31992  mdandyvrx6  31993  mdandyvrx7  31994  dandysum2p2e4  32004  usgra2pthspth  32185  usgra2pthlem1  32187  isfusgracl  32260  isfusgraclALT  32262  usgo0fis  32272  usgo0fisALT  32273  usgresvm1  32277  usgresvm1ALT  32281  mgmplusgiopALT  32351  sgrp2sgrp  32385  isrnghm  32406  2zrngaabl  32450  rnghmsscmap2  32500  rnghmsscmap  32501  rhmsscmap2  32540  rhmsscmap  32541  funcringcsetclem8  32563  funcringcsetclem8OLD  32586  zlmodzxzlmod  32651  zlmodzxzel  32652  zlmodzxzscm  32654  zlmodzxzadd  32655  snlindsntorlem  32781  ldepspr  32784  lmod1lem2  32799  lmod1lem3  32800  lmod1lem4  32801  lmod1lem5  32802  lmodn0  32806  zlmodzxznm  32808  zlmodzxzldeplem  32809  zlmodzxzldeplem1  32811  zlmodzxzldeplem3  32813  lvecpsslmod  32818  ldepsnlinc  32819  ldepslinc  32820  dpfrac1  32876  alimp-surprise  32905  ax6e2nd  33039  uun0.1  33283  relopabVD  33409  ax6e2ndVD  33416  sb5ALTVD  33421  ax6e2ndALT  33438  bj-2upln1upl  34294  bj-vtoclgfALT  34300  ishlatiN  34782  0psubN  35175  atpsubN  35179  taupilem1  37398  pwinfi  37414
  Copyright terms: Public domain W3C validator