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

Theorem mpan2 709
Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpan2.1 𝜓
mpan2.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mpan2 (𝜑𝜒)

Proof of Theorem mpan2
StepHypRef Expression
1 mpan2.1 . . 3 𝜓
21a1i 11 . 2 (𝜑𝜓)
3 mpan2.2 . 2 ((𝜑𝜓) → 𝜒)
42, 3mpdan 705 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  mpanr12  723  mp3an23  1561  eueq2  3517  sbcgf  3638  sbcralg  3650  csbconstgf  3682  sbcnestg  4136  csbnestg  4137  csbnest1g  4140  mpteq1  4885  iinexg  4969  eusv2nf  5009  reusv2lem5  5018  nnullss  5075  xpss1  5280  xpiindi  5409  reldm0  5494  elrnmpt1s  5524  resdm  5595  residOLD  5614  eliniseg  5648  trinxp  5675  inimasn  5704  ssrnres  5726  cnveq0  5745  coi2  5809  relrelss  5816  cnviin  5829  predep  5863  ord0eln0  5936  funcnvres  6124  funimaex  6133  fnresin1  6162  fnresin2  6163  fresin  6230  dffv3  6344  ssimaex  6421  dmfco  6430  fvmpt  6440  fvmptnf  6460  fvimacnvALT  6495  dff3  6531  fsn  6561  fsn2  6562  funop  6573  fvrnressn  6587  fninfp  6600  fndifnfp  6602  fnnfpeq0  6604  elabrex  6660  f1elima  6679  fsnex  6697  fliftel1  6719  f1owe  6762  sorpssuni  7107  sorpssint  7108  eldifpw  7137  ordeleqon  7149  ordsson  7150  ssnlim  7244  2ndconst  7430  curry1  7433  tposfun  7533  tpostpos2  7538  wfr3g  7578  wfrlem14  7593  wfrlem15  7594  tfrlem10  7648  tfrlem12  7650  tfr3  7660  seqomlem1  7710  seqomlem2  7711  seqomlem4  7713  ondif2  7747  oa0  7761  om0  7762  oa1suc  7776  om1  7787  oe1  7789  oe1m  7790  omass  7825  oeoalem  7841  oeoelem  7843  nnmsucr  7870  nnm1  7893  nnm2  7894  ecelqsg  7965  xpider  7981  qsel  7989  mapdm0  8034  map0e  8057  fvdiagfn  8064  ralxpmap  8069  ixpsnf1o  8110  map1  8197  xp1en  8207  sbthlem7  8237  domunsn  8271  xpmapenlem  8288  infensuc  8299  infi  8345  finresfin  8347  diffi  8353  dif1en  8354  findcard2d  8363  unblem1  8373  unblem2  8374  unblem3  8375  unblem4  8376  isfinite2  8379  infn0  8383  unfilem1  8385  unfilem2  8386  unfir  8389  fofinf1o  8402  cnvfi  8409  pwfilem  8421  mptfi  8426  finsschain  8434  marypha2  8506  eqinf  8551  inf0  8687  trcl  8773  r1rankidb  8836  snwf  8841  unwf  8842  uniwf  8851  rankval3b  8858  rankr1a  8868  rankxplim3  8913  scott0  8918  djueq1  8937  card1  8980  pm54.43  9012  infxpenc2  9031  dfac8clem  9041  alephsuc2  9089  alephle  9097  cardaleph  9098  dfacacn  9151  dfac13  9152  dfac12lem2  9154  cdaval  9180  uncdadom  9181  cdaun  9182  cdacomen  9191  cdaassen  9192  cdadom1  9196  cdainf  9202  pwcda1  9204  ackbij1lem18  9247  cflem  9256  cflecard  9263  cfeq0  9266  cfslb  9276  cfsmolem  9280  cfcoflem  9282  cfidm  9285  isfin4-3  9325  fin23lem12  9341  fin23lem16  9345  fin23lem28  9350  fin23lem38  9359  fin23lem41  9362  fin1a2lem7  9416  fin1a2lem12  9421  fin1a2lem13  9422  hsmexlem8  9434  axcc2lem  9446  axcc3  9448  domtriomlem  9452  axdc3lem2  9461  axdc3lem4  9463  axdc4lem  9465  axcclem  9467  ac6num  9489  ttukeylem4  9522  ttukeylem7  9525  ttukey2g  9526  axdclem  9529  brdom3  9538  brdom5  9539  cardeq0  9562  unsnen  9563  konigthlem  9578  pwcfsdom  9593  canthp1lem1  9662  wunex2  9748  wuncval2  9757  eltsk2g  9761  intgru  9824  ingru  9825  grutsk  9832  axgroth6  9838  mulidpi  9896  nlt1pi  9916  indpi  9917  pinq  9937  mulidnq  9973  1idpr  10039  prlem934  10043  0idsr  10106  1idsr  10107  00sr  10108  negexsr  10111  recexsrlem  10112  sqgt0sr  10115  ax1rid  10170  axcnre  10173  ne0gt0  10330  peano2cn  10396  peano2re  10397  00id  10399  mul02lem2  10401  mul01  10403  subid  10488  subid1  10489  negid  10516  negeq0  10523  peano2cnm  10535  peano2rem  10536  lt0neg1  10722  le0neg1  10724  relin01  10740  div2neg  10936  recgt0ii  11117  divgt0i2i  11127  ledivp1i  11137  ltdivp1i  11138  peano5nni  11211  peano2nn  11220  nnge1  11234  times2  11334  addltmul  11456  nn0p1nn  11520  peano2nn0  11521  nn0lele2xi  11536  frnnn0fsupp  11538  peano2z  11606  peano2zm  11608  suprzcl  11645  zeo  11651  uzwo  11940  uzwo2  11941  infssuzle  11960  infssuzcl  11961  rpnnen1lem1  12004  rpnnen1lem3  12005  rpnnen1lem5  12007  rpnnen1lem1OLD  12010  rpnnen1lem3OLD  12011  rpnnen1lem5OLD  12013  rphalfcl  12047  zgt1rpn0n1  12060  ltpnf  12143  nltmnf  12152  pnfge  12153  nltpnft  12184  xlemnf  12187  qsqueeze  12221  xlt0neg1  12239  xle0neg1  12241  xaddpnf1  12246  xaddmnf1  12248  xaddid1  12261  xsubge0  12280  xmul01  12286  xmulneg1  12288  xmulpnf1  12293  xmulid1  12298  supxrbnd  12347  supxrgtmnf  12348  supxrre1  12349  supxrre2  12350  elioopnf  12456  elicopnf  12458  xrge0neqmnf  12465  iccshftri  12496  iccshftli  12498  iccdili  12500  icccntri  12502  fzprval  12590  fz0add1fz1  12728  fzofzp1  12755  fzostep1  12774  injresinj  12779  flge0nn0  12811  flge1nn  12812  btwnzge0  12819  modfrac  12873  om2uzsuci  12937  axdc4uzlem  12972  ser1const  13047  exp0  13054  exp1  13056  expn1  13060  nn0sqcl  13077  expubnd  13111  sqval  13112  sqeq0  13117  resqcl  13121  zsqcl  13124  binom21  13170  expnbnd  13183  nn0opthlem2  13246  bcnn  13289  bcn2  13296  bcn2p1  13302  bcnm1  13304  hasheq0  13342  hashsng  13347  hashen1  13348  hashin  13387  hashdif  13389  hashxplem  13408  hashf1lem2  13428  hash2pr  13439  hash2prde  13440  pr2pwpr  13449  hash3tr  13460  iswrd  13489  wrdval  13490  wrdv  13502  ccatval2  13546  ccatrid  13555  s111  13582  swrd0len0  13632  repsw0  13720  repsw1  13726  cshw0  13736  wwlktovf  13896  relexpsucnnl  13967  shftfib  14007  reim0  14053  imval2  14086  cjne0  14098  abssq  14241  max0add  14245  abs2dif  14267  rddif  14275  absrdbnd  14276  rexuz3  14283  rlimdm  14477  isershft  14589  isercolllem2  14591  isercoll  14593  fsum  14646  fsumadd  14665  fsumsplitsnun  14679  fsumsplitsnunOLD  14681  bcxmas  14762  infcvgaux2i  14785  fprod  14866  risefac0  14953  fallfac0  14954  risefac1  14959  fallfac1  14960  bpoly2  14983  bpoly3  14984  bpoly4  14985  fsumcube  14986  efi4p  15062  resin4p  15063  recos4p  15064  sinbnd  15105  cosbnd  15106  znnenlem  15135  rpnnen2lem8  15145  rpnnen2lem12  15149  cnso  15171  dvdsmul2  15202  dvdslelem  15229  odd2np1lem  15262  mod2eq1n2dvds  15269  divalglem0  15314  divalglem1  15315  divalglem4  15317  divalglem5  15318  divalglem8  15321  flodddiv4  15335  bits0  15348  bitsp1o  15353  bitsf1  15366  sadadd2lem2  15370  gcd1  15447  gcdmultiple  15467  lcm0val  15505  dvdslcm  15509  lcmeq0  15511  lcmgcd  15518  lcm1  15521  lcmfunsnlem2lem2  15550  lcmfunsnlem2  15551  prm2orodd  15602  phiprm  15680  pc0  15757  pcdvdstr  15778  vdwlem2  15884  vdwlem6  15888  vdwlem8  15890  hashbc0  15907  setsval  16086  fsets  16089  setsres  16099  ressinbas  16134  ressress  16136  elrestr  16287  pwssnf1o  16356  xpsfrnel  16421  ismred2  16461  submre  16463  mreacs  16516  oppchomfval  16571  brssc  16671  isssc  16677  yonedalem4c  17114  isprs  17127  oduleval  17328  oduclatb  17341  gsumval2a  17476  mulg1  17745  mulgnegnn  17748  isghm  17857  ghmghmrn  17876  cntrnsg  17970  oppgplusfval  17974  psgneldm2i  18121  efgrelexlemb  18359  frgp0  18369  frgpmhm  18374  vrgpf  18377  cygctb  18489  dprd0  18626  dprd2da  18637  mgpplusg  18689  opprmulfval  18821  subrgint  19000  lsp0  19207  sralem  19375  rlmval2  19392  fczpsrbag  19565  ply1idvr1  19861  evls1rhmlem  19884  evl1fval1lem  19892  zringcyg  20037  mulgrhm2  20045  zlmsca  20067  chrnzr  20076  zrhpsgnelbas  20138  ocvz  20220  cssincl  20230  css0  20231  css1  20232  frlmip  20315  mat1scmat  20543  marrepeval  20567  decpmatid  20773  0opn  20907  topopn  20909  basdif0  20955  tgval  20957  isopn2  21034  0cld  21040  ntropn  21051  ntrval2  21053  ntrdif  21054  clsdif  21055  cmclsopn  21064  clstop  21071  ntrtop  21072  cls0  21082  ntr0  21083  mretopd  21094  neips  21115  neiptopnei  21134  maxlp  21149  isperf2  21154  rest0  21171  iocpnfordt  21217  icomnfordt  21218  mnfnei  21223  refref  21514  unisngl  21528  1stckgen  21555  ptbasfi  21582  pthaus  21639  imasnopn  21691  imasncld  21692  imasncls  21693  fbssfi  21838  isfil2  21857  ssfg  21873  filconn  21884  fbasrn  21885  filufint  21921  imaelfm  21952  fmfnfmlem4  21958  fclsfnflim  22028  alexsubALTlem3  22050  alexsubALTlem4  22051  ustfilxp  22213  ustuqtop1  22242  ustuqtop2  22243  ustuqtop3  22244  ustuqtop4  22245  utopsnneiplem  22248  utopsnnei  22250  utop2nei  22251  cfiluweak  22296  neipcfilu  22297  xmetres  22366  metres  22367  mopnex  22521  prdsms  22533  blval2  22564  metucn  22573  tngds  22649  tngngp3  22657  nmoge0  22722  cnfldnm  22779  tgioo  22796  xrtgioo  22806  xrsmopn  22812  negcncf  22918  phtpy01  22981  pco0  23010  tchtopn  23221  tchnmfval  23223  caussi  23291  rrxip  23374  minveclem3b  23395  ovolfioo  23432  ovolficc  23433  ovolfsf  23436  ovolctb  23454  ovolctb2  23456  ovolfiniun  23465  ovoliun2  23470  ovolshftlem1  23473  ovolscalem1  23477  ovolicopnf  23488  iunmbl2  23521  uniioombllem2  23547  opnmblALT  23567  ismbf  23592  mbfinf  23627  0plef  23634  itg1climres  23676  itg2cnlem1  23723  iblitg  23730  ibl0  23748  itgcn  23804  cnlimc  23847  dvfre  23909  dvnfre  23910  dveflem  23937  dvef  23938  dvlipcn  23952  lhop2  23973  itgsubstlem  24006  deg1val  24051  ply1rem  24118  coefv0  24199  plyrecj  24230  vieta1lem2  24261  aannenlem1  24278  aaliou2b  24291  ulmval  24329  ulmpm  24332  ulmdvlem1  24349  mtest  24353  efcn  24392  sin2pim  24432  cos2pim  24433  sinmpi  24434  cosmpi  24435  sinppi  24436  cosppi  24437  efimpi  24438  sincosq1lem  24444  sincosq2sgn  24446  sincosq3sgn  24447  sincosq4sgn  24448  sinq12gt0  24454  sinq34lt0t  24456  sincosq1eq  24459  abssinper  24465  efif1o  24487  loglt1b  24575  relogcn  24579  ellogdm  24580  efopn  24599  cxp0  24611  cxp1  24612  cxpsqrt  24644  logsqrt  24645  logb1  24702  atandm3  24800  atanbnd  24848  atancn  24858  leibpi  24864  efrlim  24891  logdifbnd  24915  vmaprm  25038  ppip1le  25082  ppieq0  25097  prmorcht  25099  ppiublem1  25122  ppiub  25124  chpeq0  25128  chtub  25132  fsumvma  25133  pclogsum  25135  chpval2  25138  dchrresb  25179  dchrptlem1  25184  lgs0  25230  lgs2  25234  lgsdir2lem2  25246  lgsdir2lem4  25248  lgsdchrval  25274  lgsdchr  25275  lgseisenlem2  25296  2lgslem1c  25313  2lgsoddprmlem2  25329  dirith2  25412  selberg2lem  25434  qabvle  25509  qabvexp  25510  ostth  25523  istrkg2ld  25554  ttgval  25950  cchhllem  25962  brbtwn  25974  colinearalglem4  25984  upgr0eop  26204  uspgrushgr  26265  usgruspgr  26268  usgr0eop  26333  0grsubgr  26365  dfnbgr2  26425  nbuhgr  26434  uspgrloopvtx  26617  umgr2v2evtx  26623  usgr0edg0rusgr  26677  rgrusgrprc  26691  wlkvtxiedg  26726  pthdivtx  26831  usgr2pthlem  26865  wlkpwwlkf1ouspgr  26984  wwlksext2clwwlk  27183  wwlksext2clwwlkOLD  27184  konigsbergssiedgw  27398  frgrncvvdeqlem7  27455  2clwwlk2  27501  numclwwlk2lem1OLD  27540  ex-po  27599  pliguhgr  27645  nvnd  27848  ipval2lem3  27865  ipval2  27867  ipidsq  27870  dipcj  27874  dip0r  27877  nmlnogt0  27957  blocni  27965  ipasslem2  27992  ipasslem8  27997  ipasslem9  27998  ajval  28022  ubthlem1  28031  hvaddid2  28185  hvsub0  28238  hi02  28259  hlimi  28350  isch2  28385  chlimi  28396  chsupunss  28508  shsupunss  28510  chlejb1i  28640  h1dei  28714  h1de2ci  28720  spanunsni  28743  pjoml2i  28749  pjorthi  28833  mayete3i  28892  hosubid1  28962  nmopge0  29075  nmfnge0  29091  adj1  29097  adjeq  29099  lnop0  29130  lnopmi  29164  nmophmi  29195  cnlnadjlem5  29235  cnlnadjeui  29241  unierri  29268  leoprf2  29291  leopnmid  29302  nmopleid  29303  hstles  29395  hst0  29397  strlem3a  29416  dmdbr2  29467  mdsl1i  29485  mdsl2i  29486  mdsl2bi  29487  cvmdi  29488  mdslmd1lem1  29489  mdslmd1lem2  29490  mdslmd1i  29493  mdslmd2i  29494  csmdsymi  29498  mdexchi  29499  superpos  29518  atomli  29546  atordi  29548  chirredlem1  29554  chirredlem2  29555  atcvat4i  29561  atabsi  29565  mdsymlem1  29567  mdsymlem5  29571  mdsymlem6  29572  sumdmdii  29579  dmdbr5ati  29586  dmdbr6ati  29587  mddmdin0i  29595  cdj3lem2  29599  xppreima  29754  abfmpunirn  29757  abfmpel  29760  aciunf1lem  29767  fgreu  29776  imafi2  29794  padct  29802  fpwrelmapffslem  29812  fpwrelmap  29813  xrge0infss  29830  xrdifh  29847  clatp0cl  29976  clatp1cl  29977  resvval  30132  rearchi  30147  locfinreflem  30212  locfinref  30213  ordtconnlem1  30275  rge0scvg  30300  lmxrge0  30303  qqh0  30333  qqh1  30334  rrh0  30364  zrhre  30368  esumcst  30430  esumfzf  30436  esumfsupre  30438  hasheuni  30452  sgon  30492  dmvlsiga  30497  sigainb  30504  measval  30566  ismeas  30567  sxbrsigalem0  30638  omssubadd  30667  carsggect  30685  eulerpartlemmf  30742  eulerpartlemgs2  30747  eulerpartlemn  30748  rrvsum  30821  ballotlem2  30855  ballotlemfcc  30860  ballotlem4  30865  signsplypnf  30932  signsply0  30933  signsw0glem  30935  signswrid  30940  signlem0  30969  bnj535  31263  bnj580  31286  bnj907  31338  bnj1253  31388  ptpconn  31518  cvmsss2  31559  cvmlift2lem12  31599  cvmlift2lem13  31600  cvmliftphtlem  31602  cvmliftpht  31603  mppsthm  31779  bcneg1  31925  fprb  31972  opelco3  31979  fv1stcnv  31981  fv2ndcnv  31982  trpred0  32037  wlimeq1  32067  frr3g  32081  noextendseq  32122  noetalem3  32167  scutun12  32219  funpartfv  32354  imagesset  32362  altopeq1  32372  brcolinear2  32467  gtinfOLD  32616  cldbnd  32623  ivthALT  32632  refssfne  32655  tailfb  32674  ontgval  32732  onint1  32750  axc11n11r  32975  bj-restsn10  33341  bj-restsnid  33342  bj-rest10  33343  bj-rest0  33348  bj-inftyexpiinv  33402  bj-inftyexpidisj  33404  taupilem1  33474  f1omptsnlem  33490  mptsnunlem  33492  topdifinffinlem  33502  finixpnum  33703  tan2h  33710  matunitlindflem2  33715  ptrest  33717  poimirlem22  33740  poimirlem25  33743  mblfinlem1  33755  mblfinlem2  33756  mblfinlem3  33757  mblfinlem4  33758  ismblfin  33759  itg2addnclem  33770  itg2addnclem2  33771  itg2addnclem3  33772  itg2addnc  33773  itg2gt0cn  33774  ftc1anclem5  33798  ftc1anclem8  33801  dvasin  33805  dvacos  33806  sdclem2  33847  totbndbnd  33897  heibor1lem  33917  heiborlem7  33925  bfplem1  33930  prnc  34175  el2v2  34308  brxrn  34455  riotasv  34744  glbconN  35162  atpointN  35528  polsubN  35692  pol0N  35694  pol1N  35695  2polvalN  35699  2polssN  35700  3polN  35701  pcl0N  35707  2pmaplubN  35711  pnonsingN  35718  polsubclN  35737  cdlemefs32sn1aw  36200  cdleme43fsv1snlem  36206  cdleme41sn3a  36219  cdleme32a  36227  cdleme40m  36253  cdleme40n  36254  cdleme42b  36264  istendo  36546  cdlemk40  36703  cdlemkid  36722  dihvalcqpre  37022  mapfzcons1cl  37779  eldioph3b  37826  eldiophss  37836  0dioph  37840  vdioph  37841  eldioph4b  37873  eldioph4i  37874  rencldnfilem  37882  rmxy1  37985  rmxy0  37986  rmxm1  37997  rmym1  37998  monotoddzzfi  38005  aomclem6  38127  pwslnmlem0  38159  pwslnmlem1  38160  isnumbasabl  38174  areaquad  38300  relexp2  38467  eltrclrec  38470  elrtrclrec  38471  brtrclrec  38486  brrtrclrec  38487  relexpxpmin  38507  dftrcl3  38510  dfrtrcl3  38523  heeq1  38569  seff  39006  lhe4.4ex1a  39026  eelT0  39500  snssl  39560  sineq0ALT  39668  elabrexg  39701  elrnmpt1sf  39871  founiiun0  39872  mapdm0OLD  39878  supxrgere  40043  supxrgelem  40047  fmuldfeqlem1  40313  fmuldfeq  40314  climneg  40341  sumnnodd  40361  liminfltlem  40535  addccncf2  40588  dvsinax  40626  stoweidlem18  40734  stoweidlem19  40735  stoweidlem22  40738  stoweidlem34  40750  stoweidlem40  40756  stoweidlem41  40757  stoweidlem55  40771  stoweidlem59  40775  dirker2re  40808  dirkerdenne0  40809  fourierdlem48  40870  fourierdlem49  40871  fourierdlem70  40892  fourierdlem71  40893  fourierdlem104  40926  fourierdlem112  40934  fouriersw  40947  etransclem46  40996  etransclem48  40998  nnfoctbdjlem  41171  rlimdmafv  41759  fsummmodsnunz  41851  flsqrt5  42015  bits0ALTV  42096  mogoldbblem  42135  sgoldbeven3prm  42177  nnsum3primes4  42182  uspgrsprfo  42262  2zrngnmlid  42455  2zrngnmrid  42456  mpt2exxg2  42622  lco0  42722  zlmodzxzldeplem3  42797  0dig1  42909  aacllem  43056
  Copyright terms: Public domain W3C validator