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  3526  ssini  3568  bm1.3ii  4411  epelg  4628  elvv  4892  funpr  5464  mpt2v  6175  caovcom  6255  1st2val  6597  2nd2val  6598  elxp7  6604  tfr1a  6845  oeoa  7028  oeoe  7030  erov  7189  th3q  7201  endisj  7390  phplem2  7483  snopfsupp  7635  cantnffvalOLD  7863  r1funlim  7965  dfac2  8292  cflecard  8414  canth4  8806  canthnumlem  8807  canthwelem  8809  canthp1lem2  8812  pwfseqlem4  8821  wunex3  8900  recexsrlem  9262  mulcani  9967  div1  10015  recdiv  10029  divdiv1  10034  divdiv2  10035  div23i  10081  div11i  10082  divmuldivi  10083  divadddivi  10085  divdivdivi  10086  lemulge11  10183  negiso  10298  dfnn3  10328  2cnne0  10528  2rene0  10529  halfpm6th  10538  avglt1  10554  avglt2  10555  x2times  11254  xrsupsslem  11261  xrinfmsslem  11262  injresinjlem  11630  om2uzoi  11770  fzennn  11782  expge1  11893  faclbnd2  12059  faclbnd4lem1  12061  hashf  12102  hashsnlei  12162  hashunlei  12167  hashsslei  12168  hash2prd  12173  lsw0g  12260  repswccat  12415  cshwsexa  12450  f1oun2prg  12519  wrdlen2i  12538  cjreb  12604  sqr2gt1lt2  12756  abs1m  12815  amgm2  12849  climcndslem2  13305  efcllem  13355  ege2le3  13367  efi4p  13413  efival  13428  sin01bnd  13461  cos01bnd  13462  cos1bnd  13463  cos2bnd  13464  cos01gt0  13467  sin02gt0  13468  sincos2sgn  13470  sin4lt0  13471  egt2lt3  13480  rpnnen2lem3  13491  rpnnen2lem11  13499  nthruc  13525  nthruz  13526  divalglem5  13593  ndvdsi  13606  bitsp1o  13621  pcrec  13917  prmrec  13975  modsubi  14093  structfn  14179  strlemor0  14256  strlemor1  14257  strleun  14260  sscres  14728  ga0  15807  symg2bas  15894  f1otrspeq  15944  0frgp  16267  srgbinomlem4  16629  psrbag0  17551  psrbagsn  17552  coe1mul2  17698  evls1sca  17733  cnfld1  17816  cnsubdrglem  17839  expmhm  17855  expghm  17898  expghmOLD  17899  matmulr  18288  m2detleib  18412  smadiadetglem1  18452  isbasis3g  18529  fctop  18583  cctop  18585  bl2in  19950  dscmet  20140  iihalf1  20478  iihalf2  20480  icopnfhmeo  20490  iccpnfhmeo  20492  xrhmeo  20493  minveclem2  20888  minveclem4  20894  ovolunlem1a  20954  volf  20987  i1f1lem  21142  mbfi1fseqlem5  21172  dveflem  21426  pilem2  21892  pilem3  21893  sinhalfpilem  21900  sincosq1lem  21934  tangtx  21942  sinq12gt0  21944  sincos4thpi  21950  sincos6thpi  21952  sincos3rdpi  21953  pige3  21954  coseq1  21959  efeq1  21960  efif1olem4  21976  angneg  22174  ang180lem1  22180  1cubrlem  22211  quart1  22226  log2cnv  22314  log2tlbnd  22315  log2ublem1  22316  log2ub  22319  emcllem1  22364  emcllem6  22369  basellem1  22393  basellem2  22394  basellem3  22395  basellem8  22400  ppiublem1  22516  ppiublem2  22517  ppiub  22518  chtublem  22525  chtub  22526  bcmono  22591  bclbnd  22594  bpos1lem  22596  bposlem1  22598  bposlem2  22599  bposlem3  22600  bposlem4  22601  bposlem5  22602  bposlem6  22603  bposlem7  22604  bposlem8  22605  bposlem9  22606  lgsdir2lem1  22637  chebbnd1lem1  22693  chebbnd1lem3  22695  chebbnd1  22696  dchrisum0flblem2  22733  dchrisum0lem1  22740  mulog2sumlem2  22759  selberglem2  22770  chpdifbndlem1  22777  ercgrg  22944  axlowdimlem4  23142  axlowdimlem5  23143  axlowdimlem6  23144  axlowdimlem7  23145  axlowdimlem8  23146  axlowdimlem10  23148  axlowdimlem11  23149  usgraexvlem  23264  usgraexmpldifpr  23269  0trl  23396  2trllemH  23402  2trllemE  23403  2wlklemA  23404  2wlklemB  23405  2wlklemC  23406  wlkntrllem2  23410  wlkntrl  23412  0pth  23420  0pthonv  23431  constr1trl  23438  1pthon  23441  1pthon2v  23443  constr2spth  23450  constr2pth  23451  2pthon  23452  2pthon3v  23454  constr3lem1  23482  constr3lem4  23484  constr3trllem3  23489  constr3pthlem2  23493  ex-natded5.2i  23564  ex-an  23580  ex-id  23592  ex-po  23593  ex-fl  23605  cnrngo  23841  nvz0  24007  ipidsq  24059  ipdirilem  24180  siilem1  24202  minvecolem2  24227  minvecolem3  24228  minvecolem4  24232  hvsubcan  24427  hvsubcan2  24428  normlem7tALT  24472  helch  24597  hsn0elch  24602  hhshsslem2  24620  hhsssh  24621  shscli  24671  shintcli  24683  shintcl  24684  chintcli  24685  chintcl  24686  shincli  24716  shsval2i  24741  omlsi  24758  chincli  24814  chabs1  24870  fh1i  24975  fh2i  24976  cm2ji  24979  pjnormi  25075  nmopsetn0  25220  nmfnsetn0  25233  lnophm  25374  nmcexi  25381  nmbdfnlb  25405  imaelshi  25413  nlelshi  25415  nmopadjlem  25444  nmopcoadji  25456  hmopidmch  25508  hmopidmpj  25509  sto1i  25591  stlei  25595  stji1i  25597  csmdsymi  25689  chirred  25750  cdj3lem1  25789  xrsclat  26092  reofld  26260  nn0archi  26263  xrge0iifmhm  26321  cnzh  26351  rezh  26352  qqh0  26365  qqh1  26366  rerrext  26390  cnrrext  26391  prsiga  26526  oms0  26662  coinfliprv  26817  ballotlem1  26821  ballotth  26872  signsw0g  26909  signswmnd  26910  subfacval2  27027  erdszelem2  27032  cvmliftlem4  27129  problem4  27253  4bc2eq6  27342  dfpo2  27516  br6  27518  dfon2lem3  27549  poseq  27665  wfrlem13  27687  wfr3  27693  fullfunfnv  27928  bpoly3  28152  onpsstopbas  28228  sin2h  28375  cos2h  28376  tan2h  28377  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  dvtanlem  28394  itg2addnclem2  28397  asindmre  28432  fneref  28509  refref  28510  filnetlem2  28553  filnetlem3  28554  heiborlem7  28669  riscer  28747  ac6s6f  28938  mzpclall  29016  diophin  29064  diophun  29065  eldioph4b  29103  irrapx1  29122  2nn0ind  29239  aomclem4  29363  lhe4.4ex1a  29556  expgrowth  29562  fnchoice  29704  itgsinexplem1  29747  stoweidlem13  29761  stoweidlem14  29762  stoweidlem26  29774  stoweidlem34  29782  stoweidlem49  29797  stoweidlem59  29807  astbstanbst  29876  aistbistaandb  29877  abnotataxb  29884  mdandyv0  29893  mdandyv1  29894  mdandyv2  29895  mdandyv3  29896  mdandyv4  29897  mdandyv5  29898  mdandyv6  29899  mdandyv7  29900  mdandyv8  29901  mdandyv9  29902  mdandyv10  29903  mdandyv11  29904  mdandyv12  29905  mdandyv13  29906  mdandyv14  29907  mdandyv15  29908  mdandyvr0  29909  mdandyvr1  29910  mdandyvr2  29911  mdandyvr3  29912  mdandyvr4  29913  mdandyvr5  29914  mdandyvr6  29915  mdandyvr7  29916  mdandyvrx0  29925  mdandyvrx1  29926  mdandyvrx2  29927  mdandyvrx3  29928  mdandyvrx4  29929  mdandyvrx5  29930  mdandyvrx6  29931  mdandyvrx7  29932  dandysum2p2e4  29942  hash2prv  30179  wlkcomp  30239  usgra2pthspth  30248  usgra2wlkspthlem1  30249  usgra2wlkspthlem2  30250  usgra2pthlem1  30253  usgra2adedgspth  30258  usgra2adedgwlk  30259  usgra2adedgwlkon  30260  usg2wlk  30262  usg2wlkon  30263  el2wlkonot  30341  el2spthonot  30342  el2spthonot0  30343  usg2wlkonot  30355  usg2wotspth  30356  clwlkcomp  30379  frgrancvvdgeq  30589  numclwwlk1  30644  numclwwlk2lem3  30652  frgraregord013  30664  zlmodzxzlmod  30702  zlmodzxzel  30703  zlmodzxzscm  30705  zlmodzxzadd  30706  psgnsn  30722  coe1fsupp  30769  mat1dimelbas  30790  snlindsntorlem  30893  ldepspr  30896  lmod1lem2  30919  lmod1lem3  30920  lmod1lem4  30921  lmod1lem5  30922  lmodn0  30926  zlmodzxznm  30928  zlmodzxzldeplem  30929  zlmodzxzldeplem1  30931  zlmodzxzldeplem3  30933  lvecpsslmod  30938  ldepsnlinc  30939  ldepslinc  30940  dpfrac1  30996  alimp-surprise  31019  ax6e2nd  31154  uun0.1  31398  relopabVD  31524  ax6e2ndVD  31531  sb5ALTVD  31536  ax6e2ndALT  31553  bj-2upln1upl  32364  bj-vtoclgfALT  32365  ishlatiN  32840  0psubN  33233  atpsubN  33237  taupilem1  35455
  Copyright terms: Public domain W3C validator