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

Theorem pm3.2i 469
Description: Infer conjunction of premises. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
pm3.2i.1 𝜑
pm3.2i.2 𝜓
Assertion
Ref Expression
pm3.2i (𝜑𝜓)

Proof of Theorem pm3.2i
StepHypRef Expression
1 pm3.2i.1 . 2 𝜑
2 pm3.2i.2 . 2 𝜓
3 pm3.2 461 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
41, 2, 3mp2 9 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wa 382
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 195  df-an 384
This theorem is referenced by:  pm4.87  605  dfbi  658  mp4an  704  3pm3.2i  1231  unssi  3746  elini  3755  ssini  3794  bm1.3ii  4703  epelg  4937  elvv  5087  funpr  5841  funcnvpr  5847  mpt2v  6623  caovcom  6703  1st2val  7059  2nd2val  7060  elxp7  7066  wfrlem13  7288  wfr3  7296  tfr1a  7351  oeoa  7538  oeoe  7540  erov  7705  endisj  7906  phplem2  7999  snopfsupp  8155  r1funlim  8486  dfac2  8810  cflecard  8932  canth4  9322  canthnumlem  9323  canthwelem  9325  canthp1lem2  9328  pwfseqlem4  9337  wunex3  9416  addsrpr  9749  mulsrpr  9750  recexsrlem  9777  mulcani  10512  div1  10562  recdiv  10577  divdiv1  10582  divdiv2  10583  div23i  10629  div11i  10630  divmuldivi  10631  divadddivi  10633  divdivdivi  10634  lemulge11  10731  negiso  10847  dfnn3  10878  2cnne0  11086  2rene0  11087  halfpm6th  11097  avglt1  11114  avglt2  11115  div4p1lem1div2  11131  3halfnz  11285  divlt1lt  11728  divle1le  11729  nnledivrp  11769  x2times  11955  xrsupsslem  11962  xrinfmsslem  11963  fz0to4untppr  12263  fldiv4lem1div2uz2  12451  om2uzoi  12568  fzennn  12581  expge1  12711  sqoddm1div8  12842  faclbnd2  12892  faclbnd4lem1  12894  4bc2eq6  12930  hashf  12938  hashsnlei  13016  hashunlei  13021  hashsslei  13022  hash2prb  13060  repswccat  13326  cshwsexa  13364  funcnvs4  13453  f1oun2prg  13455  wrdlen2i  13477  relexpaddg  13584  cjreb  13654  sqrt2gt1lt2  13806  abs1m  13866  amgm2  13900  climcndslem2  14364  fprodn0f  14504  bpoly3  14571  efcllem  14590  ege2le3  14602  efi4p  14649  efival  14664  sin01bnd  14697  cos01bnd  14698  cos1bnd  14699  cos2bnd  14700  sin01gt0  14702  cos01gt0  14703  sin02gt0  14704  sincos2sgn  14706  sin4lt0  14707  egt2lt3  14716  rpnnen2lem3  14727  rpnnen2lem11  14735  nthruc  14762  nthruz  14763  3dvdsdec  14835  3dvdsdecOLD  14836  3dvds2dec  14837  3dvds2decOLD  14838  mod2eq1n2dvds  14852  oddge22np1  14854  halfleoddlt  14867  nno  14879  divalglem5  14901  ndvdsi  14917  flodddiv4  14918  flodddiv4lt  14920  flodddiv4t2lthalf  14921  bitsp1o  14936  3lcm2e6woprm  15109  6lcm4e12  15110  pcrec  15344  prmrec  15407  prmo1  15522  prmgaplcmlem1  15536  prmgaplcm  15545  modsubi  15557  structfn  15651  strlemor0  15738  strlemor1  15739  strleun  15742  isofn  16201  sscres  16249  funcestrcsetclem7  16552  funcestrcsetclem8  16553  fullestrcsetc  16557  mgmnsgrpex  17184  ga0  17497  symg2bas  17584  f1otrspeq  17633  psgnsn  17706  0frgp  17958  gsummptnn0fz  18148  srgbinomlem4  18309  psrbag0  19258  psrbagsn  19259  coe1fsupp  19348  coe1mul2  19403  evls1sca  19452  cnfld1  19533  cnsubdrglem  19559  expmhm  19577  expghm  19605  matmulr  20002  mat1dimelbas  20035  mat1f1o  20042  m2detleib  20195  smadiadetglem1  20235  pmatcollpw3fi1lem2  20350  cpmidpmatlem2  20434  cpmadumatpolylem1  20444  cayhamlem3  20450  cayhamlem4  20451  isbasis3g  20503  fctop  20557  cctop  20559  refref  21065  bl2in  21953  dscmet  22125  iihalf1  22466  iihalf2  22468  icopnfhmeo  22478  iccpnfhmeo  22480  xrhmeo  22481  iscvsi  22663  ncvs1  22688  minveclem2  22919  minveclem4  22925  ovolunlem1a  22985  volf  23018  i1f1lem  23176  mbfi1fseqlem5  23206  dveflem  23460  pilem2  23924  pilem3  23925  sinhalfpilem  23933  sincosq1lem  23967  tangtx  23975  sinq12gt0  23977  sincos4thpi  23983  sincos6thpi  23985  sincos3rdpi  23986  pige3  23987  coseq1  23992  efeq1  23993  efif1olem4  24009  logblog  24244  angneg  24247  ang180lem1  24253  1cubrlem  24282  quart1  24297  log2cnv  24385  log2tlbnd  24386  log2ublem1  24387  log2ub  24390  emcllem1  24436  emcllem6  24441  basellem1  24521  basellem2  24522  basellem3  24523  basellem8  24528  ppiublem1  24641  ppiublem2  24642  ppiub  24643  chtublem  24650  chtub  24651  bcmono  24716  bclbnd  24719  bpos1lem  24721  bposlem1  24723  bposlem2  24724  bposlem3  24725  bposlem4  24726  bposlem5  24727  bposlem6  24728  bposlem7  24729  bposlem8  24730  bposlem9  24731  lgsdir2lem1  24764  1lgs  24779  gausslemma2dlem0c  24797  gausslemma2dlem0d  24798  gausslemma2dlem1a  24804  gausslemma2dlem2  24806  gausslemma2dlem3  24807  gausslemma2dlem5  24810  gausslemma2dlem6  24811  lgsquad2lem2  24824  2lgslem1a1  24828  2lgslem1a2  24829  2lgslem1c  24832  2lgslem3a  24835  2lgslem3b  24836  2lgslem3c  24837  2lgslem3d  24838  2lgslem3  24843  2lgsoddprmlem1  24847  chebbnd1lem1  24872  chebbnd1lem3  24874  chebbnd1  24875  dchrisum0flblem2  24912  dchrisum0lem1  24919  mulog2sumlem2  24938  selberglem2  24949  chpdifbndlem1  24956  ercgrg  25127  axlowdimlem4  25540  axlowdimlem5  25541  axlowdimlem6  25542  axlowdimlem7  25543  axlowdimlem8  25544  axlowdimlem10  25546  axlowdimlem11  25547  usgraexmpldifpr  25691  usgraexmpledg  25695  wlkcomp  25816  0trl  25839  2trllemH  25845  2trllemE  25846  2wlklemA  25847  2wlklemB  25848  2wlklemC  25849  wlkntrllem2  25853  wlkntrl  25855  0pth  25863  0pthonv  25874  constr1trl  25881  1pthon  25884  1pthon2v  25886  constr2spth  25893  constr2pth  25894  2pthon  25895  2pthon3v  25897  usgra2adedgspth  25904  usgra2adedgwlk  25905  usgra2adedgwlkon  25906  usg2wlk  25908  usg2wlkon  25909  usgra2wlkspthlem1  25910  usgra2wlkspthlem2  25911  constr3lem1  25936  constr3lem4  25938  constr3trllem3  25943  constr3pthlem2  25947  clwlkcomp  26054  el2wlkonot  26159  el2spthonot  26160  el2spthonot0  26161  usg2wlkonot  26173  usg2wotspth  26174  frgraregord013  26408  ex-natded5.2i  26418  ex-an  26434  ex-id  26446  ex-po  26447  ex-fl  26459  ex-mod  26461  ex-exp  26462  ex-lcm  26470  nvz0  26698  ipidsq  26750  ipdirilem  26871  siilem1  26893  minvecolem2  26918  minvecolem3  26919  minvecolem4  26923  hvsubcan  27118  hvsubcan2  27119  normlem7tALT  27163  helch  27287  hsn0elch  27292  hhshsslem2  27312  hhsssh  27313  shscli  27363  shintcli  27375  shintcl  27376  chintcli  27377  chintcl  27378  shincli  27408  shsval2i  27433  omlsi  27450  chincli  27506  chabs1  27562  fh1i  27667  fh2i  27668  cm2ji  27671  pjnormi  27767  nmopsetn0  27911  nmfnsetn0  27924  lnophm  28065  nmcexi  28072  nmbdfnlb  28096  imaelshi  28104  nlelshi  28106  nmopadjlem  28135  nmopcoadji  28147  hmopidmch  28199  hmopidmpj  28200  sto1i  28282  stlei  28286  stji1i  28288  csmdsymi  28380  chirred  28441  cdj3lem1  28480  xrsclat  28814  nn0archi  28977  lmatfvlem  29012  xrge0iifmhm  29116  qqh0  29159  qqh1  29160  rerrext  29184  cnrrext  29185  prsiga  29324  oms0  29489  coinfliprv  29674  ballotlem1  29678  ballotth  29729  signsw0g  29762  subfacval2  30226  erdszelem2  30231  cvmliftlem4  30327  elmrsubrn  30474  msubfval  30478  problem4  30619  quad3  30621  dfpo2  30701  br6  30703  dfon2lem3  30737  poseq  30797  fullfunfnv  31026  fneref  31318  filnetlem2  31347  filnetlem3  31348  onpsstopbas  31402  dnizeq0  31438  dnibndlem12  31452  knoppcnlem5  31460  knoppcnlem8  31463  knoppcnlem10  31465  knoppcnlem11  31466  knoppndvlem14  31489  cnndvlem1  31501  bj-genr  31579  bj-genl  31580  bj-genan  31581  bj-2upln1upl  32005  bj-vtoclgfALT  32012  bj-toprntopon  32044  bj-pwnex  32046  taupilem1  32144  topdifinf  32173  sin2h  32369  cos2h  32370  tan2h  32371  pigt3  32372  poimirlem1  32380  poimirlem2  32381  poimirlem3  32382  poimirlem4  32383  poimirlem6  32385  poimirlem7  32386  poimirlem11  32390  poimirlem12  32391  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  poimirlem22  32401  poimirlem23  32402  poimirlem24  32403  poimirlem25  32404  poimirlem26  32405  poimirlem29  32408  poimirlem31  32410  mblfinlem3  32418  mblfinlem4  32419  ismblfin  32420  itg2addnclem2  32432  asindmre  32465  heiborlem7  32586  riscer  32757  ac6s6f  32951  ishlatiN  33460  0psubN  33853  atpsubN  33857  mzpclall  36108  diophin  36154  diophun  36155  eldioph4b  36193  irrapx1  36210  2nn0ind  36328  aomclem4  36445  ifpid3g  36656  ifpid2g  36657  ifpbi1b  36667  pwinfi  36688  rtrclex  36743  cnvrcl0  36751  dfrcl2  36785  relexp1idm  36825  relexp0idm  36826  clsk1independent  37164  lhe4.4ex1a  37350  expgrowth  37356  ax6e2nd  37595  uun0.1  37826  relopabVD  37959  ax6e2ndVD  37966  sb5ALTVD  37971  ax6e2ndALT  37988  fnchoice  38011  dvmptconst  38604  dvmptidg  38606  dvmulcncf  38616  dvdivcncf  38618  dvnprodlem3  38639  itgsinexplem1  38646  volioof  38681  stoweidlem13  38707  stoweidlem14  38708  stoweidlem26  38720  stoweidlem34  38728  stoweidlem49  38743  stoweidlem59  38753  dirkertrigeqlem3  38794  dirkercncflem1  38797  dirkercncflem2  38798  fourierdlem57  38857  fourierdlem62  38862  fourierdlem103  38903  fourierdlem111  38911  fourierswlem  38924  fouriersw  38925  salexct2  39034  salexct3  39037  salgencntex  39038  salgensscntex  39039  gsumge0cl  39065  sge00  39070  sge0tsms  39074  0ome  39220  ovnlecvr  39249  ovn0lem  39256  hoidmvle  39291  ovnsubadd2lem  39336  smflimlem6  39463  mbfpsssmf  39470  smfmullem4  39480  smfpimbor1lem1  39484  astbstanbst  39526  aistbistaandb  39527  abnotataxb  39533  aifftbifffaibif  39538  confun4  39559  plcofph  39561  plvcofph  39563  plvcofphax  39564  plvofpos  39565  mdandyv0  39566  mdandyv1  39567  mdandyv2  39568  mdandyv3  39569  mdandyv4  39570  mdandyv5  39571  mdandyv6  39572  mdandyv7  39573  mdandyv8  39574  mdandyv9  39575  mdandyv10  39576  mdandyv11  39577  mdandyv12  39578  mdandyv13  39579  mdandyv14  39580  mdandyv15  39581  mdandyvr0  39582  mdandyvr1  39583  mdandyvr2  39584  mdandyvr3  39585  mdandyvr4  39586  mdandyvr5  39587  mdandyvr6  39588  mdandyvr7  39589  mdandyvrx0  39598  mdandyvrx1  39599  mdandyvrx2  39600  mdandyvrx3  39601  mdandyvrx4  39602  mdandyvrx5  39603  mdandyvrx6  39604  mdandyvrx7  39605  dandysum2p2e4  39615  fmtno4prmfac  39824  31prm  39852  lighneallem4a  39865  41prothprmlem2  39875  zofldiv2ALTV  39914  gbegt5  39985  gbogt5  39986  gboage9  39988  9gboa  39998  11gboa  39999  nnsum3primes4  40006  nnsum3primesgbe  40010  nnsum4primesodd  40014  nnsum4primesoddALTV  40015  nnsum4primeseven  40018  nnsum4primesevenALTV  40019  tgblthelfgott  40031  tgoldbach  40034  tgblthelfgottOLD  40038  tgoldbachOLD  40041  pfx2  40077  mptmpt2opabbrd  40159  structvtxvallem  40252  graop  40261  grastruct  40262  uhgrunop  40299  usgrop  40392  usgr2v1e2w  40477  usgrexmpledg  40485  uhgrsubgrself  40503  uhgrspan1lem1  40523  upgrres1lem1  40527  fusgrfis  40548  vtxd0nedgb  40702  p1evtxdeqlem  40727  p1evtxdeq  40728  p1evtxdp1  40729  umgr2v2e  40740  vdegp1bi-av  40752  1wlkcomp  40834  upgr2pthnlp  40937  usgr2trlncl  40965  usgr2pthlem  40968  clWlkcomp  40985  uspgrn2crct  41010  wspthnonp  41054  21wlkond  41143  2pthond  41148  2pthon3v-av  41149  umgr2adedgwlkonALT  41153  umgr2wlk  41155  umgr2wlkon  41156  umgrwwlks2on  41160  wpthswwlks2on  41163  elwspths2spth  41170  0ewlk  41281  0pth-av  41292  0pthonv-av  41296  1pthon2v-av  41319  31wlkdlem4  41328  3trlond  41339  3pthond  41341  3spthond  41343  trlsegvdeglem3  41389  eupthvdres  41402  eupth2lemb  41404  mgmplusgiopALT  41619  sgrp2sgrp  41653  isrnghm  41681  2zrngaabl  41733  rnghmsscmap2  41764  rnghmsscmap  41765  funcrngcsetc  41789  funcrngcsetcALT  41790  rhmsscmap2  41810  rhmsscmap  41811  funcringcsetc  41826  funcringcsetcALTV2lem8  41834  funcringcsetclem8ALTV  41857  zlmodzxzlmod  41924  zlmodzxzel  41925  zlmodzxzscm  41927  zlmodzxzadd  41928  snlindsntorlem  42052  ldepspr  42055  lmod1lem2  42070  lmod1lem3  42071  lmod1lem4  42072  lmod1lem5  42073  lmodn0  42077  zlmodzxznm  42079  zlmodzxzldeplem  42080  zlmodzxzldeplem1  42082  zlmodzxzldeplem3  42084  lvecpsslmod  42089  ldepsnlinc  42090  ldepslinc  42091  expnegico01  42101  zofldiv2  42118  flnn0div2ge  42120  elbigo2  42143  nnlog2ge0lt1  42157  digfval  42188  dignnld  42194  dignn0flhalf  42209  dpfrac1  42272  dpfrac1OLD  42273  alimp-surprise  42295  aacllem  42316
  Copyright terms: Public domain W3C validator