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

Theorem mpan2 706
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 701 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  mpanr12  720  mp3an23  1413  eueq2  3367  sbcgf  3488  sbcralg  3500  csbconstgf  3531  sbcnestg  3975  csbnestg  3976  csbnest1g  3979  mpteq1  4707  iinexg  4794  eusv2nf  4834  reusv2lem5  4843  nnullss  4901  xpss1  5199  xpiindi  5227  reldm0  5313  elrnmpt1s  5343  resdm  5410  resid  5429  eliniseg  5463  trinxp  5490  inimasn  5519  ssrnres  5541  cnveq0  5560  coi2  5621  relrelss  5628  cnviin  5641  predep  5675  ord0eln0  5748  funcnvres  5935  funimaex  5944  fnresin1  5973  fnresin2  5974  fresin  6040  dffv3  6154  ssimaex  6230  dmfco  6239  fvmpt  6249  fvmptnf  6268  fvimacnvALT  6302  dff3  6338  fsn  6367  fsn2  6368  funop  6379  fvrnressn  6393  fninfp  6405  fndifnfp  6407  fnnfpeq0  6409  elabrex  6466  f1elima  6485  fsnex  6503  fliftel1  6525  f1owe  6568  sorpssuni  6911  sorpssint  6912  eldifpw  6938  ordeleqon  6950  ordsson  6951  ssnlim  7045  2ndconst  7226  curry1  7229  tposfun  7328  tpostpos2  7333  wfr3g  7373  wfrlem14  7388  wfrlem15  7389  tfrlem10  7443  tfrlem12  7445  tfr3  7455  seqomlem1  7505  seqomlem2  7506  seqomlem4  7508  ondif2  7542  oa0  7556  om0  7557  oa1suc  7571  om1  7582  oe1  7584  oe1m  7585  omass  7620  oeoalem  7636  oeoelem  7638  nnmsucr  7665  nnm1  7688  nnm2  7689  ecelqsg  7762  xpider  7778  qsel  7786  mapdm0  7832  map0e  7855  fvdiagfn  7862  ralxpmap  7867  ixpsnf1o  7908  map1  7996  xp1en  8006  sbthlem7  8036  domunsn  8070  xpmapenlem  8087  infensuc  8098  infi  8144  finresfin  8146  diffi  8152  dif1en  8153  findcard2d  8162  unblem1  8172  unblem2  8173  unblem3  8174  unblem4  8175  isfinite2  8178  infn0  8182  unfilem1  8184  unfilem2  8185  unfir  8188  fofinf1o  8201  cnvfi  8208  pwfilem  8220  mptfi  8225  finsschain  8233  marypha2  8305  eqinf  8350  inf0  8478  trcl  8564  r1rankidb  8627  snwf  8632  unwf  8633  uniwf  8642  rankval3b  8649  rankr1a  8659  rankxplim3  8704  scott0  8709  card1  8754  pm54.43  8786  infxpenc2  8805  dfac8clem  8815  alephsuc2  8863  alephle  8871  cardaleph  8872  dfacacn  8923  dfac13  8924  dfac12lem2  8926  cdaval  8952  uncdadom  8953  cdaun  8954  cdacomen  8963  cdaassen  8964  cdadom1  8968  cdainf  8974  pwcda1  8976  ackbij1lem18  9019  cflem  9028  cflecard  9035  cfeq0  9038  cfslb  9048  cfsmolem  9052  cfcoflem  9054  cfidm  9057  isfin4-3  9097  fin23lem12  9113  fin23lem16  9117  fin23lem28  9122  fin23lem38  9131  fin23lem41  9134  fin1a2lem7  9188  fin1a2lem12  9193  fin1a2lem13  9194  hsmexlem8  9206  axcc2lem  9218  axcc3  9220  domtriomlem  9224  axdc3lem2  9233  axdc3lem4  9235  axdc4lem  9237  axcclem  9239  ac6num  9261  ttukeylem4  9294  ttukeylem7  9297  ttukey2g  9298  axdclem  9301  brdom3  9310  brdom5  9311  cardeq0  9334  unsnen  9335  konigthlem  9350  pwcfsdom  9365  canthp1lem1  9434  wunex2  9520  wuncval2  9529  eltsk2g  9533  intgru  9596  ingru  9597  grutsk  9604  axgroth6  9610  mulidpi  9668  nlt1pi  9688  indpi  9689  pinq  9709  mulidnq  9745  1idpr  9811  prlem934  9815  0idsr  9878  1idsr  9879  00sr  9880  negexsr  9883  recexsrlem  9884  sqgt0sr  9887  ax1rid  9942  axcnre  9945  ne0gt0  10102  peano2cn  10168  peano2re  10169  00id  10171  mul02lem2  10173  mul01  10175  subid  10260  subid1  10261  negid  10288  negeq0  10295  peano2cnm  10307  peano2rem  10308  lt0neg1  10494  le0neg1  10496  relin01  10512  div2neg  10708  recgt0ii  10889  divgt0i2i  10899  ledivp1i  10909  ltdivp1i  10910  peano5nni  10983  peano2nn  10992  nnge1  11006  times2  11106  addltmul  11228  nn0p1nn  11292  peano2nn0  11293  nn0lele2xi  11308  frnnn0fsupp  11310  peano2z  11378  peano2zm  11380  suprzcl  11417  zeo  11423  uzwo  11711  uzwo2  11712  infssuzle  11731  infssuzcl  11732  rpnnen1lem1  11775  rpnnen1lem3  11776  rpnnen1lem5  11778  rpnnen1lem1OLD  11781  rpnnen1lem3OLD  11782  rpnnen1lem5OLD  11784  rphalfcl  11818  zgt1rpn0n1  11831  ltpnf  11914  nltmnf  11923  pnfge  11924  nltpnft  11955  qsqueeze  11991  xlt0neg1  12009  xle0neg1  12011  xaddpnf1  12016  xaddmnf1  12018  xaddid1  12031  xsubge0  12050  xmul01  12056  xmulneg1  12058  xmulpnf1  12063  xmulid1  12068  supxrbnd  12117  supxrgtmnf  12118  supxrre1  12119  supxrre2  12120  elioopnf  12225  elicopnf  12227  xrge0neqmnf  12234  iccshftri  12265  iccshftli  12267  iccdili  12269  icccntri  12271  fzprval  12359  fz0add1fz1  12494  fzofzp1  12522  fzostep1  12540  injresinj  12545  flge0nn0  12577  flge1nn  12578  btwnzge0  12585  modfrac  12639  om2uzsuci  12703  axdc4uzlem  12738  ser1const  12813  exp0  12820  exp1  12822  expn1  12826  nn0sqcl  12843  expubnd  12877  sqval  12878  sqeq0  12883  resqcl  12887  zsqcl  12890  binom21  12936  expnbnd  12949  nn0opthlem2  13012  bcnn  13055  bcn2  13062  bcn2p1  13068  bcnm1  13070  hasheq0  13110  hashsng  13115  hashen1  13116  hashin  13155  hashdif  13157  hashxplem  13176  hashf1lem2  13194  hash2pr  13205  hash2prde  13206  pr2pwpr  13215  hash3tr  13227  iswrd  13262  wrdval  13263  wrdv  13275  ccatval2  13317  ccatrid  13325  s111  13350  swrd0len0  13390  repsw0  13477  repsw1  13483  cshw0  13493  wwlktovf  13649  relexpsucnnl  13722  shftfib  13762  reim0  13808  imval2  13841  cjne0  13853  abssq  13996  max0add  14000  abs2dif  14022  rddif  14030  absrdbnd  14031  rexuz3  14038  rlimdm  14232  isershft  14344  isercolllem2  14346  isercoll  14348  fsum  14400  fsumadd  14419  fsumsplitsnun  14433  bcxmas  14511  infcvgaux2i  14534  fprod  14615  risefac0  14702  fallfac0  14703  risefac1  14708  fallfac1  14709  bpoly2  14732  bpoly3  14733  bpoly4  14734  fsumcube  14735  efi4p  14811  resin4p  14812  recos4p  14813  sinbnd  14854  cosbnd  14855  znnenlem  14884  rpnnen2lem8  14894  rpnnen2lem12  14898  cnso  14920  dvdsmul2  14947  dvdslelem  14974  odd2np1lem  15007  mod2eq1n2dvds  15014  divalglem0  15059  divalglem1  15060  divalglem4  15062  divalglem5  15063  divalglem8  15066  flodddiv4  15080  bits0  15093  bitsp1o  15098  bitsf1  15111  sadadd2lem2  15115  gcd1  15192  gcdmultiple  15212  lcm0val  15250  dvdslcm  15254  lcmeq0  15256  lcmgcd  15263  lcm1  15266  lcmfunsnlem2lem2  15295  lcmfunsnlem2  15296  prm2orodd  15347  phiprm  15425  pc0  15502  pcdvdstr  15523  vdwlem2  15629  vdwlem6  15633  vdwlem8  15635  hashbc0  15652  setsval  15828  fsets  15831  setsres  15841  ressinbas  15876  ressress  15878  elrestr  16029  pwssnf1o  16098  xpsfrnel  16163  ismred2  16203  submre  16205  mreacs  16259  oppchomfval  16314  brssc  16414  isssc  16420  yonedalem4c  16857  isprs  16870  oduleval  17071  oduclatb  17084  gsumval2a  17219  mulg1  17488  mulgnegnn  17491  isghm  17600  ghmghmrn  17619  cntrnsg  17714  oppgplusfval  17718  psgneldm2i  17865  efgrelexlemb  18103  frgp0  18113  frgpmhm  18118  vrgpf  18121  cygctb  18233  dprd0  18370  dprd2da  18381  mgpplusg  18433  opprmulfval  18565  subrgint  18742  lsp0  18949  sralem  19117  rlmval2  19134  fczpsrbag  19307  ply1idvr1  19603  evls1rhmlem  19626  evl1fval1lem  19634  zringcyg  19779  mulgrhm2  19787  zlmsca  19809  chrnzr  19818  zrhpsgnelbas  19880  ocvz  19962  cssincl  19972  css0  19973  css1  19974  frlmip  20057  mat1scmat  20285  marrepeval  20309  decpmatid  20515  0opn  20649  topopn  20651  basdif0  20697  tgval  20699  isopn2  20776  0cld  20782  ntropn  20793  ntrval2  20795  ntrdif  20796  clsdif  20797  cmclsopn  20806  clstop  20813  ntrtop  20814  cls0  20824  ntr0  20825  mretopd  20836  neips  20857  neiptopnei  20876  maxlp  20891  isperf2  20896  rest0  20913  iocpnfordt  20959  icomnfordt  20960  mnfnei  20965  refref  21256  unisngl  21270  1stckgen  21297  ptbasfi  21324  pthaus  21381  imasnopn  21433  imasncld  21434  imasncls  21435  fbssfi  21581  isfil2  21600  ssfg  21616  filconn  21627  fbasrn  21628  filufint  21664  imaelfm  21695  fmfnfmlem4  21701  fclsfnflim  21771  alexsubALTlem3  21793  alexsubALTlem4  21794  ustfilxp  21956  ustuqtop1  21985  ustuqtop2  21986  ustuqtop3  21987  ustuqtop4  21988  utopsnneiplem  21991  utopsnnei  21993  utop2nei  21994  cfiluweak  22039  neipcfilu  22040  xmetres  22109  metres  22110  mopnex  22264  prdsms  22276  blval2  22307  metucn  22316  tngds  22392  tngngp3  22400  nmoge0  22465  cnfldnm  22522  tgioo  22539  xrtgioo  22549  xrsmopn  22555  negcncf  22661  phtpy01  22724  pco0  22754  tchtopn  22965  tchnmfval  22967  caussi  23035  rrxip  23118  minveclem3b  23139  ovolfioo  23176  ovolficc  23177  ovolfsf  23180  ovolctb  23198  ovolctb2  23200  ovolfiniun  23209  ovoliun2  23214  ovolshftlem1  23217  ovolscalem1  23221  ovolicopnf  23232  iunmbl2  23265  uniioombllem2  23291  opnmblALT  23311  ismbf  23337  mbfinf  23372  0plef  23379  itg1climres  23421  itg2cnlem1  23468  iblitg  23475  ibl0  23493  itgcn  23549  cnlimc  23592  dvfre  23654  dvnfre  23655  dveflem  23680  dvef  23681  dvlipcn  23695  lhop2  23716  itgsubstlem  23749  deg1val  23794  ply1rem  23861  coefv0  23942  plyrecj  23973  vieta1lem2  24004  aannenlem1  24021  aaliou2b  24034  ulmval  24072  ulmpm  24075  ulmdvlem1  24092  mtest  24096  efcn  24135  sin2pim  24175  cos2pim  24176  sinmpi  24177  cosmpi  24178  sinppi  24179  cosppi  24180  efimpi  24181  sincosq1lem  24187  sincosq2sgn  24189  sincosq3sgn  24190  sincosq4sgn  24191  sinq12gt0  24197  sinq34lt0t  24199  sincosq1eq  24202  abssinper  24208  efif1o  24230  relogcn  24318  ellogdm  24319  efopn  24338  cxp0  24350  cxp1  24351  cxpsqrt  24383  logsqrt  24384  logb1  24441  atandm3  24539  atanbnd  24587  atancn  24597  leibpi  24603  efrlim  24630  logdifbnd  24654  vmaprm  24777  ppip1le  24821  ppieq0  24836  prmorcht  24838  ppiublem1  24861  ppiub  24863  chpeq0  24867  chtub  24871  fsumvma  24872  pclogsum  24874  chpval2  24877  dchrresb  24918  dchrptlem1  24923  lgs0  24969  lgs2  24973  lgsdir2lem2  24985  lgsdir2lem4  24987  lgsdchrval  25013  lgsdchr  25014  lgseisenlem2  25035  2lgslem1c  25052  2lgsoddprmlem2  25068  dirith2  25151  selberg2lem  25173  qabvle  25248  qabvexp  25249  ostth  25262  istrkg2ld  25293  ttgval  25689  cchhllem  25701  brbtwn  25713  colinearalglem4  25723  upgr0eop  25938  uspgrushgr  25997  usgruspgr  26000  usgr0eop  26065  0grsubgr  26097  dfnbgr2  26156  nbuhgr  26160  uspgrloopvtx  26331  umgr2v2evtx  26337  usgr0edg0rusgr  26375  rgrusgrprc  26389  wlkvtxiedg  26424  pthdivtx  26528  usgr2pthlem  26562  wlkpwwlkf1ouspgr  26668  wwlksext2clwwlk  26824  konigsbergssiedgw  27011  frgrncvvdeqlemA  27068  numclwwlk2lem1  27124  ex-po  27180  pliguhgr  27226  nvnd  27431  ipval2lem3  27448  ipval2  27450  ipidsq  27453  dipcj  27457  dip0r  27460  nmlnogt0  27540  blocni  27548  ipasslem2  27575  ipasslem8  27580  ipasslem9  27581  ajval  27605  ubthlem1  27614  hvaddid2  27768  hvsub0  27821  hi02  27842  hlimi  27933  isch2  27968  chlimi  27979  chsupunss  28091  shsupunss  28093  chlejb1i  28223  h1dei  28297  h1de2ci  28303  spanunsni  28326  pjoml2i  28332  pjorthi  28416  mayete3i  28475  hosubid1  28545  nmopge0  28658  nmfnge0  28674  adj1  28680  adjeq  28682  lnop0  28713  lnopmi  28747  nmophmi  28778  cnlnadjlem5  28818  cnlnadjeui  28824  unierri  28851  leoprf2  28874  leopnmid  28885  nmopleid  28886  hstles  28978  hst0  28980  strlem3a  28999  dmdbr2  29050  mdsl1i  29068  mdsl2i  29069  mdsl2bi  29070  cvmdi  29071  mdslmd1lem1  29072  mdslmd1lem2  29073  mdslmd1i  29076  mdslmd2i  29077  csmdsymi  29081  mdexchi  29082  superpos  29101  atomli  29129  atordi  29131  chirredlem1  29137  chirredlem2  29138  atcvat4i  29144  atabsi  29148  mdsymlem1  29150  mdsymlem5  29154  mdsymlem6  29155  sumdmdii  29162  dmdbr5ati  29169  dmdbr6ati  29170  mddmdin0i  29178  cdj3lem2  29182  xppreima  29332  abfmpunirn  29335  abfmpel  29338  aciunf1lem  29345  fgreu  29355  imafi2  29373  padct  29381  fpwrelmapffslem  29391  fpwrelmap  29392  xlemnf  29400  xrge0infss  29410  xrdifh  29427  clatp0cl  29498  clatp1cl  29499  resvval  29654  rearchi  29669  locfinreflem  29731  locfinref  29732  ordtconnlem1  29794  rge0scvg  29819  lmxrge0  29822  qqh0  29852  qqh1  29853  rrh0  29883  zrhre  29887  esumcst  29948  esumfzf  29954  esumfsupre  29956  hasheuni  29970  sgon  30010  dmvlsiga  30015  sigainb  30022  measval  30084  ismeas  30085  sxbrsigalem0  30156  omssubadd  30185  carsggect  30203  eulerpartlemmf  30260  eulerpartlemgs2  30265  eulerpartlemn  30266  rrvsum  30339  ballotlem2  30373  ballotlemfcc  30378  ballotlem4  30383  signsplypnf  30449  signsply0  30450  signsw0glem  30452  signswrid  30457  signlem0  30486  bnj535  30721  bnj580  30744  bnj907  30796  bnj1253  30846  ptpconn  30976  cvmsss2  31017  cvmlift2lem12  31057  cvmlift2lem13  31058  cvmliftphtlem  31060  cvmliftpht  31061  mppsthm  31237  bcneg1  31383  fprb  31426  opelco3  31433  fv1stcnv  31435  fv2ndcnv  31436  trpred0  31490  wlimeq1  31520  frr3g  31533  noxpsgn  31572  noextendltgt  31627  funpartfv  31747  imagesset  31755  altopeq1  31765  brcolinear2  31860  gtinfOLD  32009  cldbnd  32016  ivthALT  32025  refssfne  32048  tailfb  32067  ontgval  32125  onint1  32143  axc11n11r  32368  bj-restsn10  32729  bj-restsnid  32730  bj-rest10  32731  bj-rest0  32736  bj-inftyexpiinv  32767  bj-inftyexpidisj  32769  taupilem1  32839  f1omptsnlem  32854  mptsnunlem  32856  topdifinffinlem  32866  finixpnum  33065  tan2h  33072  matunitlindflem2  33077  ptrest  33079  poimirlem22  33102  poimirlem25  33105  mblfinlem1  33117  mblfinlem2  33118  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  itg2addnclem  33132  itg2addnclem2  33133  itg2addnclem3  33134  itg2addnc  33135  itg2gt0cn  33136  ftc1anclem5  33160  ftc1anclem8  33163  dvasin  33167  dvacos  33168  sdclem2  33209  totbndbnd  33259  heibor1lem  33279  heiborlem7  33287  bfplem1  33292  prnc  33537  riotasv  33764  glbconN  34182  atpointN  34548  polsubN  34712  pol0N  34714  pol1N  34715  2polvalN  34719  2polssN  34720  3polN  34721  pcl0N  34727  2pmaplubN  34731  pnonsingN  34738  polsubclN  34757  cdlemefs32sn1aw  35221  cdleme43fsv1snlem  35227  cdleme41sn3a  35240  cdleme32a  35248  cdleme40m  35274  cdleme40n  35275  cdleme42b  35285  istendo  35567  cdlemk40  35724  cdlemkid  35743  dihvalcqpre  36043  mapfzcons1cl  36800  eldioph3b  36847  eldiophss  36857  0dioph  36861  vdioph  36862  eldioph4b  36894  eldioph4i  36895  rencldnfilem  36903  rmxy1  37006  rmxy0  37007  rmxm1  37018  rmym1  37019  monotoddzzfi  37026  aomclem6  37148  pwslnmlem0  37180  pwslnmlem1  37181  isnumbasabl  37196  areaquad  37322  relexp2  37489  eltrclrec  37492  elrtrclrec  37493  brtrclrec  37508  brrtrclrec  37509  relexpxpmin  37529  dftrcl3  37532  dfrtrcl3  37545  heeq1  37592  seff  38029  lhe4.4ex1a  38049  eelT0  38523  snssl  38587  sineq0ALT  38695  elabrexg  38728  elrnmpt1sf  38885  founiiun0  38886  mapdm0OLD  38892  supxrgere  39048  supxrgelem  39052  fmuldfeqlem1  39250  fmuldfeq  39251  climneg  39278  sumnnodd  39298  addccncf2  39424  dvsinax  39463  stoweidlem18  39572  stoweidlem19  39573  stoweidlem22  39576  stoweidlem34  39588  stoweidlem40  39594  stoweidlem41  39595  stoweidlem55  39609  stoweidlem59  39613  dirker2re  39646  dirkerdenne0  39647  fourierdlem48  39708  fourierdlem49  39709  fourierdlem70  39730  fourierdlem71  39731  fourierdlem104  39764  fourierdlem112  39772  fouriersw  39785  etransclem46  39834  etransclem48  39836  nnfoctbdjlem  40009  rlimdmafv  40591  fsummmodsnunz  40673  flsqrt5  40838  bits0ALTV  40919  nnsum3primes4  40995  uspgrsprfo  41074  2zrngnmlid  41267  2zrngnmrid  41268  mpt2exxg2  41434  lco0  41534  zlmodzxzldeplem3  41609  loglt1b  41650  0dig1  41725  aacllem  41880
  Copyright terms: Public domain W3C validator