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 472
Description: Infer conjunction of premises. Inference associated with pm3.2 471. Its associated deduction is jca 513 (and the double deduction is jcad 514). (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 471 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
41, 2, 3mp2 9 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wa 397
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 206  df-an 398
This theorem is referenced by:  mp4an  692  pm4.87  842  3pm3.2i  1340  unssi  4146  ssini  4192  opthhausdorff  5475  elvv  5707  elopaelxp  5722  relopabiv  5777  relopabi  5779  dfpo2  6249  funpr  6558  funcnvpr  6564  mpov  7469  caovcom  7552  snnex  7693  pwnex  7694  1st2val  7950  2nd2val  7951  elxp7  7957  opreuopreu  7967  mptmpoopabbrdOLD  8016  poxp2  8076  poseq  8091  wfrlem13OLD  8268  wfr3OLD  8285  tfr1a  8341  oeoa  8545  oeoe  8547  erov  8754  endisj  9003  phplem2OLD  9163  snopfsupp  9329  ssttrcl  9652  ttrclselem2  9663  r1funlim  9703  dfac2b  10067  cflecard  10190  canth4  10584  canthnumlem  10585  canthwelem  10587  canthp1lem2  10590  pwfseqlem4  10599  wunex3  10678  addsrpr  11012  mulsrpr  11013  recexsrlem  11040  mulcani  11795  div1  11845  recdiv  11862  divdiv1  11867  divdiv2  11868  div23i  11914  div11i  11915  divmuldivi  11916  divadddivi  11918  divdivdivi  11919  lemulge11  12018  negiso  12136  dfnn3  12168  2cnne0  12364  2rene0  12365  halfpm6th  12375  avglt1  12392  avglt2  12393  div4p1lem1div2  12409  3halfnz  12583  divlt1lt  12985  divle1le  12986  nnledivrp  13028  x2times  13219  xrsupsslem  13227  xrinfmsslem  13228  fz0to4untppr  13545  om2uzoi  13861  fzennn  13874  expge1  14006  sqoddm1div8  14147  faclbnd2  14192  faclbnd4lem1  14194  4bc2eq6  14230  hashfxnn0  14238  hashsnlei  14319  hashunlei  14326  hashsslei  14327  hash2prb  14372  repswccat  14675  cshwsexaOLD  14714  funcnvs4  14805  f1oun2prg  14807  wrdlen2i  14832  relexpaddg  14939  cjreb  15009  sqrt2gt1lt2  15160  abs1m  15221  bpoly3  15942  ege2le3  15973  efi4p  16020  efival  16035  sin01bnd  16068  cos01bnd  16069  cos1bnd  16070  cos2bnd  16071  sin01gt0  16073  cos01gt0  16074  sin02gt0  16075  sincos2sgn  16077  sin4lt0  16078  egt2lt3  16089  rpnnen2lem3  16099  rpnnen2lem11  16107  nthruc  16135  nthruz  16136  3dvdsdec  16215  3dvds2dec  16216  mod2eq1n2dvds  16230  halfleoddlt  16245  divalglem5  16280  ndvdsi  16295  flodddiv4  16296  flodddiv4lt  16298  bitsp1o  16314  3lcm2e6woprm  16492  6lcm4e12  16493  pcrec  16731  prmrec  16795  prmgaplcmlem1  16924  prmgaplcm  16933  modsubi  16945  structfn  17029  strleun  17030  slotsdifipndx  17217  slotsdifplendx  17257  slotsdifdsndx  17276  slotsdifunifndx  17283  slotsdifplendx2  17299  slotsdifocndx  17300  isofn  17659  sscres  17707  funcestrcsetclem7  18035  funcestrcsetclem8  18036  fullestrcsetc  18040  mgmnsgrpex  18742  pwmnd  18748  ga0  19079  symg2bas  19175  f1otrspeq  19230  psgnsn  19303  0frgp  19562  gsummptnn0fz  19764  srgbinomlem4  19961  cnfldfun  20811  cnfldfunALT  20812  cnfldfunALTOLD  20813  cnfld1  20825  cnsubdrglem  20851  expmhm  20869  expghm  20899  psrbag0  21473  psrbagsn  21474  coe1fsupp  21588  coe1mul2  21643  evls1sca  21692  matmulr  21790  mat1dimelbas  21823  mat1f1o  21830  m2detleib  21983  smadiadetglem1  22023  pmatcollpw3fi1lem2  22139  cpmidpmatlem2  22223  cpmadumatpolylem1  22233  cayhamlem3  22239  cayhamlem4  22240  isbasis3g  22302  fctop  22357  cctop  22359  refref  22867  bl2in  23756  dscmet  23931  iihalf1  24297  iihalf2  24299  icopnfhmeo  24309  iccpnfhmeo  24311  xrhmeo  24312  iscvsi  24495  zclmncvs  24515  ncvs1  24524  ehl2eudis  24789  minveclem2  24793  minveclem4  24799  ovolunlem1a  24863  volf  24896  i1f1lem  25056  mbfi1fseqlem5  25087  dveflem  25346  pilem2  25814  pilem3  25815  sinhalfpilem  25823  sincosq1lem  25857  tangtx  25865  sinq12gt0  25867  sincos4thpi  25873  sincos6thpi  25875  sincos3rdpi  25876  pigt3  25877  pige3ALT  25879  coseq1  25884  efeq1  25887  efif1olem4  25904  angneg  26156  ang180lem1  26162  1cubrlem  26194  quart1  26209  log2cnv  26297  log2tlbnd  26298  log2ublem1  26299  log2ub  26302  emcllem1  26348  emcllem6  26353  basellem1  26433  basellem2  26434  basellem3  26435  basellem8  26440  ppiublem1  26553  ppiublem2  26554  ppiub  26555  chtublem  26562  chtub  26563  bcmono  26628  bclbnd  26631  bpos1lem  26633  bposlem1  26635  bposlem2  26636  bposlem3  26637  bposlem4  26638  bposlem5  26639  bposlem6  26640  bposlem7  26641  bposlem8  26642  bposlem9  26643  lgsdir2lem1  26676  1lgs  26691  gausslemma2dlem0c  26709  gausslemma2dlem0d  26710  gausslemma2dlem1a  26716  gausslemma2dlem2  26718  gausslemma2dlem3  26719  gausslemma2dlem5  26722  gausslemma2dlem6  26723  lgsquad2lem2  26736  2lgslem1a1  26740  2lgslem1a2  26741  2lgslem1c  26744  2lgslem3a  26747  2lgslem3b  26748  2lgslem3c  26749  2lgslem3d  26750  2lgslem3  26755  2lgsoddprmlem1  26759  addsqrexnreu  26793  addsqnreup  26794  chebbnd1lem1  26820  chebbnd1lem3  26822  chebbnd1  26823  dchrisum0flblem2  26860  dchrisum0lem1  26867  mulog2sumlem2  26886  selberglem2  26897  chpdifbndlem1  26904  slotsinbpsd  27386  slotslnbpsd  27387  ercgrg  27462  axlowdimlem4  27897  axlowdimlem5  27898  axlowdimlem6  27899  axlowdimlem7  27900  axlowdimlem8  27901  axlowdimlem10  27903  axlowdimlem11  27904  graop  27983  grastruct  27984  uhgrunop  28029  upgrop  28048  upgrunop  28073  umgrunop  28075  usgrop  28117  usgr2v1e2w  28203  usgrexmpldifpr  28209  usgrexmpledg  28213  uhgrsubgrself  28231  uhgrspan1lem1  28251  upgrres1lem1  28260  fusgrfis  28281  vtxd0nedgb  28439  p1evtxdeqlem  28463  p1evtxdeq  28464  p1evtxdp1  28465  umgr2v2e  28476  vdegp1bi  28488  wlkcomp  28582  upgr2pthnlp  28683  usgr2trlncl  28711  usgr2pthlem  28714  clwlkcomp  28730  uspgrn2crct  28756  wwlksonvtx  28803  wspthnonp  28807  2wlkond  28885  2pthond  28890  2pthon3v  28891  umgr2adedgwlkonALT  28895  umgr2wlk  28897  umgr2wlkon  28898  wpthswwlks2on  28909  elwspths2spth  28915  0ewlk  29061  0pth  29072  0pthonv  29076  1pthon2v  29100  3wlkdlem4  29109  3trlond  29120  3pthond  29122  3spthond  29124  trlsegvdeglem3  29169  eupthvdres  29182  eupth2lemb  29184  ex-natded5.2i  29353  ex-an  29369  ex-id  29381  ex-po  29382  ex-fl  29394  ex-mod  29396  ex-exp  29397  ex-lcm  29405  nvz0  29613  ipidsq  29655  ipdirilem  29774  siilem1  29796  minvecolem2  29820  minvecolem3  29821  minvecolem4  29825  hvsubcan  30019  hvsubcan2  30020  normlem7tALT  30064  helch  30188  hsn0elch  30193  hhshsslem2  30213  hhsssh  30214  shscli  30262  shintcli  30274  shintcl  30275  chintcli  30276  chintcl  30277  shincli  30307  shsval2i  30332  omlsi  30349  chincli  30405  chabs1  30461  fh1i  30566  fh2i  30567  cm2ji  30570  pjnormi  30666  nmopsetn0  30810  nmfnsetn0  30823  lnophm  30964  nmcexi  30971  nmbdfnlb  30995  imaelshi  31003  nlelshi  31005  nmopadjlem  31034  nmopcoadji  31046  hmopidmch  31098  hmopidmpj  31099  sto1i  31181  stlei  31185  stji1i  31187  csmdsymi  31279  chirred  31340  cdj3lem1  31379  rpdp2cl  31741  dp2lt10  31743  dp2lt  31744  dp2ltc  31746  dpfrac1  31751  dplti  31764  dpgti  31765  dpexpp1  31767  dpadd3  31771  dpmul  31772  dpmul4  31773  xrsclat  31874  nn0archi  32142  lmatfvlem  32399  xrge0iifmhm  32523  qqh0  32568  qqh1  32569  rerrext  32593  cnrrext  32594  prsiga  32733  oms0  32900  coinfliprv  33085  ballotlem1  33089  ballotth  33140  signsw0g  33171  hgt750lemd  33264  hgt750lem  33267  hgt750lem2  33268  hgt750leme  33274  tgoldbachgt  33279  subfacval2  33784  erdszelem2  33789  cvmliftlem4  33885  satom  33953  satfv1  33960  sat1el2xp  33976  fmlaomn0  33987  satfdmfmla  33997  satfv1fvfmla1  34020  ex-sategoelelomsuc  34023  ex-sategoelel12  34024  prv0  34027  prv1n  34028  elmrsubrn  34117  msubfval  34121  problem4  34259  quad3  34261  br6  34333  dfon2lem3  34363  fullfunfnv  34534  fneref  34825  filnetlem2  34854  filnetlem3  34855  onpsstopbas  34905  dnizeq0  34941  dnibndlem12  34955  knoppcnlem5  34963  knoppcnlem8  34966  knoppcnlem10  34968  knoppcnlem11  34969  knoppndvlem14  34991  cnndvlem1  35003  bj-genr  35074  bj-genl  35075  bj-genan  35076  bj-2upln1upl  35498  bj-vtoclgfALT  35533  bj-brab2a1  35623  bj-opabssvv  35624  taupilem1  35795  topdifinf  35823  sin2h  36071  cos2h  36072  tan2h  36073  poimirlem1  36082  poimirlem2  36083  poimirlem3  36084  poimirlem4  36085  poimirlem6  36087  poimirlem7  36088  poimirlem11  36092  poimirlem12  36093  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem22  36103  poimirlem23  36104  poimirlem24  36105  poimirlem25  36106  poimirlem26  36107  poimirlem29  36110  poimirlem31  36112  mblfinlem3  36120  mblfinlem4  36121  ismblfin  36122  itg2addnclem2  36133  asindmre  36164  heiborlem7  36279  riscer  36450  refrelcoss3  36928  symrelcoss3  36930  ishlatiN  37820  0psubN  38215  atpsubN  38219  gcdcomnni  40449  gcdnegnni  40450  neggcdnni  40451  60gcd7e1  40465  lcmeprodgcdi  40467  lcm2un  40474  lcm3un  40475  lcmineqlem4  40492  lcmineqlem6  40494  3lexlogpow5ineq1  40514  aks4d1p1p2  40530  mzpclall  41053  diophin  41098  diophun  41099  eldioph4b  41137  irrapx1  41154  2nn0ind  41272  aomclem4  41387  onexlimgt  41580  nnoeomeqom  41649  oaomoencom  41654  oenassex  41655  succlg  41665  dflim5  41666  omabs2  41668  ifpid3g  41771  ifpid2g  41772  ifpbi1b  41782  eu0  41799  pwinfi  41843  rtrclex  41896  cnvrcl0  41904  dfrcl2  41953  relexp1idm  41993  relexp0idm  41994  clsk1independent  42325  lhe4.4ex1a  42616  expgrowth  42622  ax6e2nd  42847  uun0.1  43067  relopabVD  43190  ax6e2ndVD  43197  sb5ALTVD  43202  ax6e2ndALT  43219  rexanuz2nf  43735  dvmptconst  44163  dvmptidg  44165  dvmulcncf  44173  dvdivcncf  44175  dvnprodlem3  44196  itgsinexplem1  44202  volioof  44235  stoweidlem13  44261  stoweidlem14  44262  stoweidlem26  44274  stoweidlem34  44282  stoweidlem49  44297  stoweidlem59  44307  dirkertrigeqlem3  44348  dirkercncflem1  44351  dirkercncflem2  44352  fourierdlem57  44411  fourierdlem62  44416  fourierdlem103  44457  fourierdlem111  44465  fourierswlem  44478  fouriersw  44479  salexct2  44587  salexct3  44590  salgencntex  44591  salgensscntex  44592  gsumge0cl  44619  sge00  44624  sge0tsms  44628  0ome  44777  ovnlecvr  44806  ovn0lem  44813  hoidmvle  44848  ovnsubadd2lem  44893  smflimlem6  45024  mbfpsssmf  45031  smfmullem4  45042  smfpimbor1lem1  45046  astbstanbst  45151  aistbistaandb  45152  abnotataxb  45158  aifftbifffaibif  45163  confun4  45184  plcofph  45186  plvcofph  45188  plvcofphax  45189  plvofpos  45190  mdandyv0  45191  mdandyv1  45192  mdandyv2  45193  mdandyv3  45194  mdandyv4  45195  mdandyv5  45196  mdandyv6  45197  mdandyv7  45198  mdandyv8  45199  mdandyv9  45200  mdandyv10  45201  mdandyv11  45202  mdandyv12  45203  mdandyv13  45204  mdandyv14  45205  mdandyv15  45206  mdandyvr0  45207  mdandyvr1  45208  mdandyvr2  45209  mdandyvr3  45210  mdandyvr4  45211  mdandyvr5  45212  mdandyvr6  45213  mdandyvr7  45214  mdandyvrx0  45223  mdandyvrx1  45224  mdandyvrx2  45225  mdandyvrx3  45226  mdandyvrx4  45227  mdandyvrx5  45228  mdandyvrx6  45229  mdandyvrx7  45230  dandysum2p2e4  45240  or2expropbilem1  45273  dfnelbr2  45512  ich2exprop  45670  paireqne  45710  fmtno4prmfac  45771  31prm  45796  lighneallem4a  45807  41prothprmlem2  45817  zofldiv2ALTV  45861  nfermltl8rev  45941  nfermltl2rev  45942  nfermltlrev  45943  gbegt5  45960  gbowgt5  45961  gboge9  45963  9gbo  45973  11gbo  45974  nnsum3primes4  45987  nnsum3primesgbe  45991  nnsum4primesodd  45995  nnsum4primesoddALTV  45996  nnsum4primeseven  45999  nnsum4primesevenALTV  46000  tgblthelfgott  46014  tgoldbach  46016  isomgrref  46034  ushrisomgr  46040  nn0mnd  46120  mgmplusgiopALT  46135  sgrp2sgrp  46169  isrnghm  46197  2zrngaabl  46249  rnghmsscmap2  46278  rnghmsscmap  46279  funcrngcsetc  46303  funcrngcsetcALT  46304  rhmsscmap2  46324  rhmsscmap  46325  funcringcsetc  46340  funcringcsetcALTV2lem8  46348  funcringcsetclem8ALTV  46371  zlmodzxzlmod  46437  zlmodzxzel  46438  zlmodzxzscm  46440  zlmodzxzadd  46441  snlindsntorlem  46558  ldepspr  46561  lmod1lem2  46576  lmod1lem3  46577  lmod1lem4  46578  lmod1lem5  46579  lmodn0  46583  zlmodzxznm  46585  zlmodzxzldeplem  46586  zlmodzxzldeplem1  46588  zlmodzxzldeplem3  46590  lvecpsslmod  46595  ldepsnlinc  46596  ldepslinc  46597  expnegico01  46606  zofldiv2  46624  flnn0div2ge  46626  elbigo2  46645  nnlog2ge0lt1  46659  digfval  46690  dignnld  46696  dignn0flhalf  46711  2arymaptfo  46747  itcovalt2lem1  46768  prelrrx2  46806  eenglngeehlnmlem2  46831  rrxsphere  46841  line2  46845  line2x  46847  line2y  46848  itsclc0yqsollem2  46856  inlinecirc02plem  46879  sepfsepc  46967  alimp-surprise  47234  aacllem  47255
  Copyright terms: Public domain W3C validator