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

Theorem mpan2 707
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 703 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  721  mp3an23  1456  eueq2  3413  sbcgf  3534  sbcralg  3546  csbconstgf  3578  sbcnestg  4030  csbnestg  4031  csbnest1g  4034  mpteq1  4770  iinexg  4854  eusv2nf  4894  reusv2lem5  4903  nnullss  4960  xpss1  5161  xpiindi  5290  reldm0  5375  elrnmpt1s  5405  resdm  5476  residOLD  5495  eliniseg  5529  trinxp  5556  inimasn  5585  ssrnres  5607  cnveq0  5626  coi2  5690  relrelss  5697  cnviin  5710  predep  5744  ord0eln0  5817  funcnvres  6005  funimaex  6014  fnresin1  6043  fnresin2  6044  fresin  6111  dffv3  6225  ssimaex  6302  dmfco  6311  fvmpt  6321  fvmptnf  6341  fvimacnvALT  6376  dff3  6412  fsn  6442  fsn2  6443  funop  6454  fvrnressn  6468  fninfp  6481  fndifnfp  6483  fnnfpeq0  6485  elabrex  6541  f1elima  6560  fsnex  6578  fliftel1  6600  f1owe  6643  sorpssuni  6988  sorpssint  6989  eldifpw  7018  ordeleqon  7030  ordsson  7031  ssnlim  7125  2ndconst  7311  curry1  7314  tposfun  7413  tpostpos2  7418  wfr3g  7458  wfrlem14  7473  wfrlem15  7474  tfrlem10  7528  tfrlem12  7530  tfr3  7540  seqomlem1  7590  seqomlem2  7591  seqomlem4  7593  ondif2  7627  oa0  7641  om0  7642  oa1suc  7656  om1  7667  oe1  7669  oe1m  7670  omass  7705  oeoalem  7721  oeoelem  7723  nnmsucr  7750  nnm1  7773  nnm2  7774  ecelqsg  7845  xpider  7861  qsel  7869  mapdm0  7914  map0e  7937  fvdiagfn  7944  ralxpmap  7949  ixpsnf1o  7990  map1  8077  xp1en  8087  sbthlem7  8117  domunsn  8151  xpmapenlem  8168  infensuc  8179  infi  8225  finresfin  8227  diffi  8233  dif1en  8234  findcard2d  8243  unblem1  8253  unblem2  8254  unblem3  8255  unblem4  8256  isfinite2  8259  infn0  8263  unfilem1  8265  unfilem2  8266  unfir  8269  fofinf1o  8282  cnvfi  8289  pwfilem  8301  mptfi  8306  finsschain  8314  marypha2  8386  eqinf  8431  inf0  8556  trcl  8642  r1rankidb  8705  snwf  8710  unwf  8711  uniwf  8720  rankval3b  8727  rankr1a  8737  rankxplim3  8782  scott0  8787  card1  8832  pm54.43  8864  infxpenc2  8883  dfac8clem  8893  alephsuc2  8941  alephle  8949  cardaleph  8950  dfacacn  9001  dfac13  9002  dfac12lem2  9004  cdaval  9030  uncdadom  9031  cdaun  9032  cdacomen  9041  cdaassen  9042  cdadom1  9046  cdainf  9052  pwcda1  9054  ackbij1lem18  9097  cflem  9106  cflecard  9113  cfeq0  9116  cfslb  9126  cfsmolem  9130  cfcoflem  9132  cfidm  9135  isfin4-3  9175  fin23lem12  9191  fin23lem16  9195  fin23lem28  9200  fin23lem38  9209  fin23lem41  9212  fin1a2lem7  9266  fin1a2lem12  9271  fin1a2lem13  9272  hsmexlem8  9284  axcc2lem  9296  axcc3  9298  domtriomlem  9302  axdc3lem2  9311  axdc3lem4  9313  axdc4lem  9315  axcclem  9317  ac6num  9339  ttukeylem4  9372  ttukeylem7  9375  ttukey2g  9376  axdclem  9379  brdom3  9388  brdom5  9389  cardeq0  9412  unsnen  9413  konigthlem  9428  pwcfsdom  9443  canthp1lem1  9512  wunex2  9598  wuncval2  9607  eltsk2g  9611  intgru  9674  ingru  9675  grutsk  9682  axgroth6  9688  mulidpi  9746  nlt1pi  9766  indpi  9767  pinq  9787  mulidnq  9823  1idpr  9889  prlem934  9893  0idsr  9956  1idsr  9957  00sr  9958  negexsr  9961  recexsrlem  9962  sqgt0sr  9965  ax1rid  10020  axcnre  10023  ne0gt0  10180  peano2cn  10246  peano2re  10247  00id  10249  mul02lem2  10251  mul01  10253  subid  10338  subid1  10339  negid  10366  negeq0  10373  peano2cnm  10385  peano2rem  10386  lt0neg1  10572  le0neg1  10574  relin01  10590  div2neg  10786  recgt0ii  10967  divgt0i2i  10977  ledivp1i  10987  ltdivp1i  10988  peano5nni  11061  peano2nn  11070  nnge1  11084  times2  11184  addltmul  11306  nn0p1nn  11370  peano2nn0  11371  nn0lele2xi  11386  frnnn0fsupp  11388  peano2z  11456  peano2zm  11458  suprzcl  11495  zeo  11501  uzwo  11789  uzwo2  11790  infssuzle  11809  infssuzcl  11810  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  rphalfcl  11896  zgt1rpn0n1  11909  ltpnf  11992  nltmnf  12001  pnfge  12002  nltpnft  12033  xlemnf  12036  qsqueeze  12070  xlt0neg1  12088  xle0neg1  12090  xaddpnf1  12095  xaddmnf1  12097  xaddid1  12110  xsubge0  12129  xmul01  12135  xmulneg1  12137  xmulpnf1  12142  xmulid1  12147  supxrbnd  12196  supxrgtmnf  12197  supxrre1  12198  supxrre2  12199  elioopnf  12305  elicopnf  12307  xrge0neqmnf  12314  iccshftri  12345  iccshftli  12347  iccdili  12349  icccntri  12351  fzprval  12439  fz0add1fz1  12577  fzofzp1  12605  fzostep1  12624  injresinj  12629  flge0nn0  12661  flge1nn  12662  btwnzge0  12669  modfrac  12723  om2uzsuci  12787  axdc4uzlem  12822  ser1const  12897  exp0  12904  exp1  12906  expn1  12910  nn0sqcl  12927  expubnd  12961  sqval  12962  sqeq0  12967  resqcl  12971  zsqcl  12974  binom21  13020  expnbnd  13033  nn0opthlem2  13096  bcnn  13139  bcn2  13146  bcn2p1  13152  bcnm1  13154  hasheq0  13192  hashsng  13197  hashen1  13198  hashin  13237  hashdif  13239  hashxplem  13258  hashf1lem2  13278  hash2pr  13289  hash2prde  13290  pr2pwpr  13299  hash3tr  13310  iswrd  13339  wrdval  13340  wrdv  13352  ccatval2  13396  ccatrid  13405  s111  13432  swrd0len0  13482  repsw0  13570  repsw1  13576  cshw0  13586  wwlktovf  13745  relexpsucnnl  13816  shftfib  13856  reim0  13902  imval2  13935  cjne0  13947  abssq  14090  max0add  14094  abs2dif  14116  rddif  14124  absrdbnd  14125  rexuz3  14132  rlimdm  14326  isershft  14438  isercolllem2  14440  isercoll  14442  fsum  14495  fsumadd  14514  fsumsplitsnun  14528  fsumsplitsnunOLD  14530  bcxmas  14611  infcvgaux2i  14634  fprod  14715  risefac0  14802  fallfac0  14803  risefac1  14808  fallfac1  14809  bpoly2  14832  bpoly3  14833  bpoly4  14834  fsumcube  14835  efi4p  14911  resin4p  14912  recos4p  14913  sinbnd  14954  cosbnd  14955  znnenlem  14984  rpnnen2lem8  14994  rpnnen2lem12  14998  cnso  15020  dvdsmul2  15051  dvdslelem  15078  odd2np1lem  15111  mod2eq1n2dvds  15118  divalglem0  15163  divalglem1  15164  divalglem4  15166  divalglem5  15167  divalglem8  15170  flodddiv4  15184  bits0  15197  bitsp1o  15202  bitsf1  15215  sadadd2lem2  15219  gcd1  15296  gcdmultiple  15316  lcm0val  15354  dvdslcm  15358  lcmeq0  15360  lcmgcd  15367  lcm1  15370  lcmfunsnlem2lem2  15399  lcmfunsnlem2  15400  prm2orodd  15451  phiprm  15529  pc0  15606  pcdvdstr  15627  vdwlem2  15733  vdwlem6  15737  vdwlem8  15739  hashbc0  15756  setsval  15935  fsets  15938  setsres  15948  ressinbas  15983  ressress  15985  elrestr  16136  pwssnf1o  16205  xpsfrnel  16270  ismred2  16310  submre  16312  mreacs  16366  oppchomfval  16421  brssc  16521  isssc  16527  yonedalem4c  16964  isprs  16977  oduleval  17178  oduclatb  17191  gsumval2a  17326  mulg1  17595  mulgnegnn  17598  isghm  17707  ghmghmrn  17726  cntrnsg  17820  oppgplusfval  17824  psgneldm2i  17971  efgrelexlemb  18209  frgp0  18219  frgpmhm  18224  vrgpf  18227  cygctb  18339  dprd0  18476  dprd2da  18487  mgpplusg  18539  opprmulfval  18671  subrgint  18850  lsp0  19057  sralem  19225  rlmval2  19242  fczpsrbag  19415  ply1idvr1  19711  evls1rhmlem  19734  evl1fval1lem  19742  zringcyg  19887  mulgrhm2  19895  zlmsca  19917  chrnzr  19926  zrhpsgnelbas  19988  ocvz  20070  cssincl  20080  css0  20081  css1  20082  frlmip  20165  mat1scmat  20393  marrepeval  20417  decpmatid  20623  0opn  20757  topopn  20759  basdif0  20805  tgval  20807  isopn2  20884  0cld  20890  ntropn  20901  ntrval2  20903  ntrdif  20904  clsdif  20905  cmclsopn  20914  clstop  20921  ntrtop  20922  cls0  20932  ntr0  20933  mretopd  20944  neips  20965  neiptopnei  20984  maxlp  20999  isperf2  21004  rest0  21021  iocpnfordt  21067  icomnfordt  21068  mnfnei  21073  refref  21364  unisngl  21378  1stckgen  21405  ptbasfi  21432  pthaus  21489  imasnopn  21541  imasncld  21542  imasncls  21543  fbssfi  21688  isfil2  21707  ssfg  21723  filconn  21734  fbasrn  21735  filufint  21771  imaelfm  21802  fmfnfmlem4  21808  fclsfnflim  21878  alexsubALTlem3  21900  alexsubALTlem4  21901  ustfilxp  22063  ustuqtop1  22092  ustuqtop2  22093  ustuqtop3  22094  ustuqtop4  22095  utopsnneiplem  22098  utopsnnei  22100  utop2nei  22101  cfiluweak  22146  neipcfilu  22147  xmetres  22216  metres  22217  mopnex  22371  prdsms  22383  blval2  22414  metucn  22423  tngds  22499  tngngp3  22507  nmoge0  22572  cnfldnm  22629  tgioo  22646  xrtgioo  22656  xrsmopn  22662  negcncf  22768  phtpy01  22831  pco0  22860  tchtopn  23071  tchnmfval  23073  caussi  23141  rrxip  23224  minveclem3b  23245  ovolfioo  23282  ovolficc  23283  ovolfsf  23286  ovolctb  23304  ovolctb2  23306  ovolfiniun  23315  ovoliun2  23320  ovolshftlem1  23323  ovolscalem1  23327  ovolicopnf  23338  iunmbl2  23371  uniioombllem2  23397  opnmblALT  23417  ismbf  23442  mbfinf  23477  0plef  23484  itg1climres  23526  itg2cnlem1  23573  iblitg  23580  ibl0  23598  itgcn  23654  cnlimc  23697  dvfre  23759  dvnfre  23760  dveflem  23787  dvef  23788  dvlipcn  23802  lhop2  23823  itgsubstlem  23856  deg1val  23901  ply1rem  23968  coefv0  24049  plyrecj  24080  vieta1lem2  24111  aannenlem1  24128  aaliou2b  24141  ulmval  24179  ulmpm  24182  ulmdvlem1  24199  mtest  24203  efcn  24242  sin2pim  24282  cos2pim  24283  sinmpi  24284  cosmpi  24285  sinppi  24286  cosppi  24287  efimpi  24288  sincosq1lem  24294  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  sinq12gt0  24304  sinq34lt0t  24306  sincosq1eq  24309  abssinper  24315  efif1o  24337  loglt1b  24425  relogcn  24429  ellogdm  24430  efopn  24449  cxp0  24461  cxp1  24462  cxpsqrt  24494  logsqrt  24495  logb1  24552  atandm3  24650  atanbnd  24698  atancn  24708  leibpi  24714  efrlim  24741  logdifbnd  24765  vmaprm  24888  ppip1le  24932  ppieq0  24947  prmorcht  24949  ppiublem1  24972  ppiub  24974  chpeq0  24978  chtub  24982  fsumvma  24983  pclogsum  24985  chpval2  24988  dchrresb  25029  dchrptlem1  25034  lgs0  25080  lgs2  25084  lgsdir2lem2  25096  lgsdir2lem4  25098  lgsdchrval  25124  lgsdchr  25125  lgseisenlem2  25146  2lgslem1c  25163  2lgsoddprmlem2  25179  dirith2  25262  selberg2lem  25284  qabvle  25359  qabvexp  25360  ostth  25373  istrkg2ld  25404  ttgval  25800  cchhllem  25812  brbtwn  25824  colinearalglem4  25834  upgr0eop  26054  uspgrushgr  26115  usgruspgr  26118  usgr0eop  26183  0grsubgr  26215  dfnbgr2  26275  nbuhgr  26284  uspgrloopvtx  26467  umgr2v2evtx  26473  usgr0edg0rusgr  26527  rgrusgrprc  26541  wlkvtxiedg  26576  pthdivtx  26681  usgr2pthlem  26715  wlkpwwlkf1ouspgr  26833  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  konigsbergssiedgw  27228  frgrncvvdeqlem7  27285  2clwwlk2  27336  numclwwlk2lem1OLD  27363  ex-po  27422  pliguhgr  27468  nvnd  27671  ipval2lem3  27688  ipval2  27690  ipidsq  27693  dipcj  27697  dip0r  27700  nmlnogt0  27780  blocni  27788  ipasslem2  27815  ipasslem8  27820  ipasslem9  27821  ajval  27845  ubthlem1  27854  hvaddid2  28008  hvsub0  28061  hi02  28082  hlimi  28173  isch2  28208  chlimi  28219  chsupunss  28331  shsupunss  28333  chlejb1i  28463  h1dei  28537  h1de2ci  28543  spanunsni  28566  pjoml2i  28572  pjorthi  28656  mayete3i  28715  hosubid1  28785  nmopge0  28898  nmfnge0  28914  adj1  28920  adjeq  28922  lnop0  28953  lnopmi  28987  nmophmi  29018  cnlnadjlem5  29058  cnlnadjeui  29064  unierri  29091  leoprf2  29114  leopnmid  29125  nmopleid  29126  hstles  29218  hst0  29220  strlem3a  29239  dmdbr2  29290  mdsl1i  29308  mdsl2i  29309  mdsl2bi  29310  cvmdi  29311  mdslmd1lem1  29312  mdslmd1lem2  29313  mdslmd1i  29316  mdslmd2i  29317  csmdsymi  29321  mdexchi  29322  superpos  29341  atomli  29369  atordi  29371  chirredlem1  29377  chirredlem2  29378  atcvat4i  29384  atabsi  29388  mdsymlem1  29390  mdsymlem5  29394  mdsymlem6  29395  sumdmdii  29402  dmdbr5ati  29409  dmdbr6ati  29410  mddmdin0i  29418  cdj3lem2  29422  xppreima  29577  abfmpunirn  29580  abfmpel  29583  aciunf1lem  29590  fgreu  29599  imafi2  29617  padct  29625  fpwrelmapffslem  29635  fpwrelmap  29636  xrge0infss  29653  xrdifh  29670  clatp0cl  29799  clatp1cl  29800  resvval  29955  rearchi  29970  locfinreflem  30035  locfinref  30036  ordtconnlem1  30098  rge0scvg  30123  lmxrge0  30126  qqh0  30156  qqh1  30157  rrh0  30187  zrhre  30191  esumcst  30253  esumfzf  30259  esumfsupre  30261  hasheuni  30275  sgon  30315  dmvlsiga  30320  sigainb  30327  measval  30389  ismeas  30390  sxbrsigalem0  30461  omssubadd  30490  carsggect  30508  eulerpartlemmf  30565  eulerpartlemgs2  30570  eulerpartlemn  30571  rrvsum  30644  ballotlem2  30678  ballotlemfcc  30683  ballotlem4  30688  signsplypnf  30755  signsply0  30756  signsw0glem  30758  signswrid  30763  signlem0  30792  bnj535  31086  bnj580  31109  bnj907  31161  bnj1253  31211  ptpconn  31341  cvmsss2  31382  cvmlift2lem12  31422  cvmlift2lem13  31423  cvmliftphtlem  31425  cvmliftpht  31426  mppsthm  31602  bcneg1  31748  fprb  31795  opelco3  31802  fv1stcnv  31804  fv2ndcnv  31805  trpred0  31860  wlimeq1  31890  frr3g  31904  noextendseq  31945  noetalem3  31990  scutun12  32042  funpartfv  32177  imagesset  32185  altopeq1  32195  brcolinear2  32290  gtinfOLD  32439  cldbnd  32446  ivthALT  32455  refssfne  32478  tailfb  32497  ontgval  32555  onint1  32573  axc11n11r  32798  bj-restsn10  33164  bj-restsnid  33165  bj-rest10  33166  bj-rest0  33171  bj-inftyexpiinv  33225  bj-inftyexpidisj  33227  taupilem1  33297  f1omptsnlem  33313  mptsnunlem  33315  topdifinffinlem  33325  finixpnum  33524  tan2h  33531  matunitlindflem2  33536  ptrest  33538  poimirlem22  33561  poimirlem25  33564  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  ftc1anclem5  33619  ftc1anclem8  33622  dvasin  33626  dvacos  33627  sdclem2  33668  totbndbnd  33718  heibor1lem  33738  heiborlem7  33746  bfplem1  33751  prnc  33996  el2v2  34129  brxrn  34276  riotasv  34563  glbconN  34981  atpointN  35347  polsubN  35511  pol0N  35513  pol1N  35514  2polvalN  35518  2polssN  35519  3polN  35520  pcl0N  35526  2pmaplubN  35530  pnonsingN  35537  polsubclN  35556  cdlemefs32sn1aw  36019  cdleme43fsv1snlem  36025  cdleme41sn3a  36038  cdleme32a  36046  cdleme40m  36072  cdleme40n  36073  cdleme42b  36083  istendo  36365  cdlemk40  36522  cdlemkid  36541  dihvalcqpre  36841  mapfzcons1cl  37598  eldioph3b  37645  eldiophss  37655  0dioph  37659  vdioph  37660  eldioph4b  37692  eldioph4i  37693  rencldnfilem  37701  rmxy1  37804  rmxy0  37805  rmxm1  37816  rmym1  37817  monotoddzzfi  37824  aomclem6  37946  pwslnmlem0  37978  pwslnmlem1  37979  isnumbasabl  37993  areaquad  38119  relexp2  38286  eltrclrec  38289  elrtrclrec  38290  brtrclrec  38305  brrtrclrec  38306  relexpxpmin  38326  dftrcl3  38329  dfrtrcl3  38342  heeq1  38388  seff  38825  lhe4.4ex1a  38845  eelT0  39319  snssl  39379  sineq0ALT  39487  elabrexg  39520  elrnmpt1sf  39690  founiiun0  39691  mapdm0OLD  39697  supxrgere  39862  supxrgelem  39866  fmuldfeqlem1  40132  fmuldfeq  40133  climneg  40160  sumnnodd  40180  liminfltlem  40354  addccncf2  40407  dvsinax  40445  stoweidlem18  40553  stoweidlem19  40554  stoweidlem22  40557  stoweidlem34  40569  stoweidlem40  40575  stoweidlem41  40576  stoweidlem55  40590  stoweidlem59  40594  dirker2re  40627  dirkerdenne0  40628  fourierdlem48  40689  fourierdlem49  40690  fourierdlem70  40711  fourierdlem71  40712  fourierdlem104  40745  fourierdlem112  40753  fouriersw  40766  etransclem46  40815  etransclem48  40817  nnfoctbdjlem  40990  rlimdmafv  41578  fsummmodsnunz  41670  flsqrt5  41834  bits0ALTV  41915  mogoldbblem  41954  sgoldbeven3prm  41996  nnsum3primes4  42001  uspgrsprfo  42081  2zrngnmlid  42274  2zrngnmrid  42275  mpt2exxg2  42441  lco0  42541  zlmodzxzldeplem3  42616  0dig1  42728  aacllem  42875
  Copyright terms: Public domain W3C validator