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

Theorem mpan2 702
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 698 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  mpanr12  716  mp3an23  1407  eueq2  3346  sbcgf  3467  sbcralg  3479  csbconstgf  3510  sbcnestg  3948  csbnestg  3949  csbnest1g  3952  mpteq1  4659  iinexg  4745  eusv2nf  4784  reusv2lem5  4793  nnullss  4850  xpss1  5139  xpiindi  5166  reldm0  5250  elrnmpt1s  5280  resdm  5347  resid  5365  eliniseg  5399  trinxp  5426  inimasn  5454  ssrnres  5476  cnveq0  5494  coi2  5554  relrelss  5561  cnviin  5574  predep  5608  ord0eln0  5681  funcnvres  5866  funimaex  5875  fnresin1  5904  fnresin2  5905  fresin  5970  dffv3  6083  ssimaex  6157  dmfco  6166  fvmpt  6175  fvmptnf  6194  fvimacnvALT  6228  dff3  6264  fsn  6292  fsn2  6293  fvrnressn  6310  fninfp  6322  fndifnfp  6324  fnnfpeq0  6326  elabrex  6382  f1elima  6398  fsnex  6415  fliftel1  6437  f1owe  6480  sorpssuni  6821  sorpssint  6822  eldifpw  6845  ordeleqon  6857  ordsson  6858  ssnlim  6952  2ndconst  7130  curry1  7133  tposfun  7232  tpostpos2  7237  wfr3g  7277  wfrlem14  7292  wfrlem15  7293  tfrlem10  7347  tfrlem12  7349  tfr3  7359  seqomlem1  7409  seqomlem2  7410  seqomlem4  7412  ondif2  7446  oa0  7460  om0  7461  oa1suc  7475  om1  7486  oe1  7488  oe1m  7489  omass  7524  oeoalem  7540  oeoelem  7542  nnmsucr  7569  nnm1  7592  nnm2  7593  ecelqsg  7666  xpider  7682  qsel  7690  map0e  7758  fvdiagfn  7765  ralxpmap  7770  ixpsnf1o  7811  map1  7898  xp1en  7908  sbthlem7  7938  domunsn  7972  xpmapenlem  7989  infensuc  8000  infi  8046  finresfin  8048  diffi  8054  dif1en  8055  findcard2d  8064  unblem1  8074  unblem2  8075  unblem3  8076  unblem4  8077  isfinite2  8080  infn0  8084  unfilem1  8086  unfilem2  8087  unfir  8090  fofinf1o  8103  cnvfi  8108  pwfilem  8120  mptfi  8125  finsschain  8133  marypha2  8205  eqinf  8250  inf0  8378  trcl  8464  r1rankidb  8527  snwf  8532  unwf  8533  uniwf  8542  rankval3b  8549  rankr1a  8559  rankxplim3  8604  scott0  8609  card1  8654  pm54.43  8686  infxpenc2  8705  dfac8clem  8715  alephsuc2  8763  alephle  8771  cardaleph  8772  dfacacn  8823  dfac13  8824  dfac12lem2  8826  cdaval  8852  uncdadom  8853  cdaun  8854  cdacomen  8863  cdaassen  8864  cdadom1  8868  cdainf  8874  pwcda1  8876  ackbij1lem18  8919  cflem  8928  cflecard  8935  cfeq0  8938  cfslb  8948  cfsmolem  8952  cfcoflem  8954  cfidm  8957  isfin4-3  8997  fin23lem12  9013  fin23lem16  9017  fin23lem28  9022  fin23lem38  9031  fin23lem41  9034  fin1a2lem7  9088  fin1a2lem12  9093  fin1a2lem13  9094  hsmexlem8  9106  axcc2lem  9118  axcc3  9120  domtriomlem  9124  axdc3lem2  9133  axdc3lem4  9135  axdc4lem  9137  axcclem  9139  ac6num  9161  ttukeylem4  9194  ttukeylem7  9197  ttukey2g  9198  axdclem  9201  brdom3  9208  brdom5  9209  cardeq0  9230  unsnen  9231  konigthlem  9246  pwcfsdom  9261  canthp1lem1  9330  wunex2  9416  wuncval2  9425  eltsk2g  9429  intgru  9492  ingru  9493  grutsk  9500  axgroth6  9506  mulidpi  9564  nlt1pi  9584  indpi  9585  pinq  9605  mulidnq  9641  1idpr  9707  prlem934  9711  0idsr  9774  1idsr  9775  00sr  9776  negexsr  9779  recexsrlem  9780  sqgt0sr  9783  ax1rid  9838  axcnre  9841  ne0gt0  9993  peano2cn  10059  peano2re  10060  00id  10062  mul02lem2  10064  mul01  10066  subid  10151  subid1  10152  negid  10179  negeq0  10186  peano2cnm  10198  peano2rem  10199  lt0neg1  10385  le0neg1  10387  relin01  10403  div2neg  10599  recgt0ii  10780  divgt0i2i  10790  ledivp1i  10800  ltdivp1i  10801  peano5nni  10872  peano2nn  10881  nnge1  10895  times2  10995  addltmul  11117  nn0p1nn  11181  peano2nn0  11182  nn0lele2xi  11197  frnnn0fsupp  11199  peano2z  11253  peano2zm  11255  suprzcl  11291  zeo  11297  uzwo  11585  uzwo2  11586  infssuzle  11605  infssuzcl  11606  rpnnen1lem1  11649  rpnnen1lem3  11650  rpnnen1lem5  11652  rpnnen1lem1OLD  11655  rpnnen1lem3OLD  11656  rpnnen1lem5OLD  11658  rphalfcl  11692  zgt1rpn0n1  11705  ltpnf  11793  nltmnf  11802  pnfge  11803  nltpnft  11832  qsqueeze  11867  xlt0neg1  11885  xle0neg1  11887  xaddpnf1  11892  xaddmnf1  11894  xaddid1  11906  xsubge0  11922  xmul01  11928  xmulneg1  11930  xmulpnf1  11935  xmulid1  11940  supxrbnd  11988  supxrgtmnf  11989  supxrre1  11990  supxrre2  11991  elioopnf  12096  elicopnf  12098  xrge0neqmnf  12105  iccshftri  12136  iccshftli  12138  iccdili  12140  icccntri  12142  fzprval  12228  fzofzp1  12388  fzostep1  12403  injresinj  12408  flge0nn0  12440  flge1nn  12441  btwnzge0  12448  modfrac  12502  om2uzsuci  12566  axdc4uzlem  12601  ser1const  12676  exp0  12683  exp1  12685  expn1  12689  nn0sqcl  12706  expubnd  12740  sqval  12741  sqeq0  12746  resqcl  12750  zsqcl  12753  binom21  12799  expnbnd  12812  nn0opthlem2  12875  bcnn  12918  bcn2  12925  bcn2p1  12931  bcnm1  12933  hasheq0  12969  hashsng  12974  hashen1  12975  hashin  13014  hashdif  13016  hashxplem  13034  hashf1lem2  13051  hash2pr  13062  hash2prde  13063  pr2pwpr  13068  hash3tr  13079  iswrd  13110  wrdval  13111  wrdv  13123  ccatval2  13163  ccatrid  13171  s111  13196  swrd0len0  13236  repsw0  13323  repsw1  13329  cshw0  13339  wwlktovf  13495  relexpsucnnl  13568  shftfib  13608  reim0  13654  imval2  13687  cjne0  13699  abssq  13842  max0add  13846  abs2dif  13868  rddif  13876  absrdbnd  13877  rexuz3  13884  rlimdm  14078  isershft  14190  isercolllem2  14192  isercoll  14194  fsum  14246  fsumadd  14265  fsumsplitsnun  14276  bcxmas  14354  infcvgaux2i  14377  fprod  14458  risefac0  14545  fallfac0  14546  risefac1  14551  fallfac1  14552  bpoly2  14575  bpoly3  14576  bpoly4  14577  fsumcube  14578  efi4p  14654  resin4p  14655  recos4p  14656  sinbnd  14697  cosbnd  14698  znnenlem  14727  rpnnen2lem8  14737  rpnnen2lem12  14741  cnso  14763  dvdsmul2  14790  dvdslelem  14817  odd2np1lem  14850  mod2eq1n2dvds  14857  divalglem0  14902  divalglem1  14903  divalglem4  14905  divalglem5  14906  divalglem8  14909  flodddiv4  14923  bits0  14936  bitsp1o  14941  bitsf1  14954  sadadd2lem2  14958  gcd1  15035  gcdmultiple  15055  lcm0val  15093  dvdslcm  15097  lcmeq0  15099  lcmgcd  15106  lcm1  15109  lcmfunsnlem2lem2  15138  lcmfunsnlem2  15139  prm2orodd  15190  phiprm  15268  pc0  15345  pcdvdstr  15366  vdwlem2  15472  vdwlem6  15476  vdwlem8  15478  hashbc0  15495  setsval  15668  fsets  15671  setsres  15677  ressinbas  15711  ressress  15713  elrestr  15860  pwssnf1o  15929  xpsfrnel  15994  ismred2  16034  submre  16036  mreacs  16090  oppchomfval  16145  brssc  16245  isssc  16251  yonedalem4c  16688  isprs  16701  oduleval  16902  oduclatb  16915  gsumval2a  17050  mulg1  17319  mulgnegnn  17322  isghm  17431  ghmghmrn  17450  cntrnsg  17545  oppgplusfval  17549  psgneldm2i  17696  efgrelexlemb  17934  frgp0  17944  frgpmhm  17949  vrgpf  17952  cygctb  18064  dprd0  18201  dprd2da  18212  mgpplusg  18264  opprmulfval  18396  subrgint  18573  lsp0  18778  sralem  18946  rlmval2  18963  fczpsrbag  19136  ply1idvr1  19432  evls1rhmlem  19455  evl1fval1lem  19463  zringcyg  19603  mulgrhm2  19613  zlmsca  19635  chrnzr  19644  zrhpsgnelbas  19706  ocvz  19788  cssincl  19798  css0  19799  css1  19800  frlmip  19883  mat1scmat  20111  marrepeval  20135  decpmatid  20341  0opn  20481  topopn  20483  basdif0  20515  tgval  20517  isopn2  20593  0cld  20599  ntropn  20610  ntrval2  20612  ntrdif  20613  clsdif  20614  cmclsopn  20623  clstop  20630  ntrtop  20631  cls0  20641  ntr0  20642  mretopd  20653  neips  20674  neiptopnei  20693  maxlp  20708  isperf2  20713  rest0  20730  iocpnfordt  20776  icomnfordt  20777  mnfnei  20782  refref  21073  unisngl  21087  1stckgen  21114  ptbasfi  21141  pthaus  21198  imasnopn  21250  imasncld  21251  imasncls  21252  fbssfi  21398  isfil2  21417  ssfg  21433  filcon  21444  fbasrn  21445  filufint  21481  imaelfm  21512  fmfnfmlem4  21518  fclsfnflim  21588  alexsubALTlem3  21610  alexsubALTlem4  21611  ustfilxp  21773  ustuqtop1  21802  ustuqtop2  21803  ustuqtop3  21804  ustuqtop4  21805  utopsnneiplem  21808  utopsnnei  21810  utop2nei  21811  cfiluweak  21856  neipcfilu  21857  xmetres  21926  metres  21927  mopnex  22081  prdsms  22093  blval2  22124  metucn  22133  tngds  22209  tngngp3  22217  nmoge0  22282  cnfldnm  22339  tgioo  22354  xrtgioo  22364  xrsmopn  22370  negcncf  22476  phtpy01  22539  pco0  22569  tchtopn  22777  tchnmfval  22779  caussi  22847  rrxip  22930  minveclem3b  22951  ovolfioo  22987  ovolficc  22988  ovolfsf  22991  ovolctb  23009  ovolctb2  23011  ovolfiniun  23020  ovoliun2  23025  ovolshftlem1  23028  ovolscalem1  23032  ovolicopnf  23043  iunmbl2  23076  uniioombllem2  23101  opnmblALT  23121  ismbf  23147  mbfinf  23182  0plef  23189  itg1climres  23231  itg2cnlem1  23278  iblitg  23285  ibl0  23303  itgcn  23359  cnlimc  23402  dvfre  23464  dvnfre  23465  dveflem  23490  dvef  23491  dvlipcn  23505  lhop2  23526  itgsubstlem  23559  deg1val  23604  ply1rem  23671  coefv0  23752  plyrecj  23783  vieta1lem2  23814  aannenlem1  23831  aaliou2b  23844  ulmval  23882  ulmpm  23885  ulmdvlem1  23902  mtest  23906  efcn  23945  sin2pim  23985  cos2pim  23986  sinmpi  23987  cosmpi  23988  sinppi  23989  cosppi  23990  efimpi  23991  sincosq1lem  23997  sincosq2sgn  23999  sincosq3sgn  24000  sincosq4sgn  24001  sinq12gt0  24007  sinq34lt0t  24009  sincosq1eq  24012  abssinper  24018  efif1o  24040  relogcn  24128  ellogdm  24129  efopn  24148  cxp0  24160  cxp1  24161  cxpsqrt  24193  logsqrt  24194  logb1  24251  atandm3  24349  atanbnd  24397  atancn  24407  leibpi  24413  efrlim  24440  logdifbnd  24464  vmaprm  24587  ppip1le  24631  ppieq0  24646  prmorcht  24648  ppiublem1  24671  ppiub  24673  chpeq0  24677  chtub  24681  fsumvma  24682  pclogsum  24684  chpval2  24687  dchrresb  24728  dchrptlem1  24733  lgs0  24779  lgs2  24783  lgsdir2lem2  24795  lgsdir2lem4  24797  lgsdchrval  24823  lgsdchr  24824  lgseisenlem2  24845  2lgslem1c  24862  2lgsoddprmlem2  24878  dirith2  24961  selberg2lem  24983  qabvle  25058  qabvexp  25059  ostth  25072  istrkg2ld  25103  ttgval  25500  cchhllem  25512  brbtwn  25524  colinearalglem4  25534  uhgra0  25631  umgra0  25647  umisuhgra  25649  uslisushgra  25685  usisuslgra  25687  usgra0  25692  usgraedg4  25709  usgrafisbase  25736  usgrasscusgra  25804  uvtx01vtx  25813  usgra2adedgwlkonALT  25937  usgra2wlkspthlem2  25941  fargshiftlem  25955  usgrcyclnl2  25962  constr3trl  25980  constr3pth  25981  constr3cycl  25982  4cycl4dv  25988  wwlkn0s  26026  el2wlkonotlem  26182  usg2wlkonot  26203  usg2wotspth  26204  iseupa  26285  frgrancvvdeqlemA  26357  ex-po  26477  nvnd  26720  ipval2lem3  26737  ipval2  26739  ipidsq  26742  dipcj  26746  dip0r  26749  nmlnogt0  26829  blocni  26837  ipasslem2  26864  ipasslem8  26869  ipasslem9  26870  ajval  26894  ubthlem1  26903  hvaddid2  27057  hvsub0  27110  hi02  27131  hlimi  27222  isch2  27257  chlimi  27268  chsupunss  27380  shsupunss  27382  chlejb1i  27512  h1dei  27586  h1de2ci  27592  spanunsni  27615  pjoml2i  27621  pjorthi  27705  mayete3i  27764  hosubid1  27834  nmopge0  27947  nmfnge0  27963  adj1  27969  adjeq  27971  lnop0  28002  lnopmi  28036  nmophmi  28067  cnlnadjlem5  28107  cnlnadjeui  28113  unierri  28140  leoprf2  28163  leopnmid  28174  nmopleid  28175  hstles  28267  hst0  28269  strlem3a  28288  dmdbr2  28339  mdsl1i  28357  mdsl2i  28358  mdsl2bi  28359  cvmdi  28360  mdslmd1lem1  28361  mdslmd1lem2  28362  mdslmd1i  28365  mdslmd2i  28366  csmdsymi  28370  mdexchi  28371  superpos  28390  atomli  28418  atordi  28420  chirredlem1  28426  chirredlem2  28427  atcvat4i  28433  atabsi  28437  mdsymlem1  28439  mdsymlem5  28443  mdsymlem6  28444  sumdmdii  28451  dmdbr5ati  28458  dmdbr6ati  28459  mddmdin0i  28467  cdj3lem2  28471  xppreima  28622  abfmpunirn  28625  abfmpel  28628  aciunf1lem  28637  fgreu  28647  imafi2  28665  padct  28678  fpwrelmapffslem  28688  fpwrelmap  28689  xlemnf  28698  xrge0infss  28708  xrdifh  28725  clatp0cl  28795  clatp1cl  28796  resvval  28951  rearchi  28966  locfinreflem  29028  locfinref  29029  ordtconlem1  29091  rge0scvg  29116  lmxrge0  29119  qqh0  29149  qqh1  29150  rrh0  29180  zrhre  29184  esumcst  29245  esumfzf  29251  esumfsupre  29253  hasheuni  29267  sgon  29307  dmvlsiga  29312  sigainb  29319  measval  29381  ismeas  29382  sxbrsigalem0  29453  omssubadd  29482  carsggect  29500  eulerpartlemmf  29557  eulerpartlemgs2  29562  eulerpartlemn  29563  rrvsum  29636  ballotlem2  29670  ballotlemfcc  29675  ballotlem4  29680  signsplypnf  29746  signsply0  29747  signsw0glem  29749  signswrid  29754  signlem0  29783  bnj535  30007  bnj580  30030  bnj907  30082  bnj1253  30132  ptpcon  30262  cvmsss2  30303  cvmlift2lem12  30343  cvmlift2lem13  30344  cvmliftphtlem  30346  cvmliftpht  30347  mppsthm  30523  bcneg1  30668  fprb  30709  opelco3  30716  fv1stcnv  30718  fv2ndcnv  30719  trpred0  30773  wlimeq1  30803  frr3g  30816  noxpsgn  30855  funpartfv  31015  imagesset  31023  altopeq1  31033  brcolinear2  31128  gtinfOLD  31277  cldbnd  31284  ivthALT  31293  refssfne  31316  tailfb  31335  ontgval  31393  onint1  31411  axc11n11r  31653  bj-restsn10  32003  bj-restsnid  32004  bj-rest10  32005  bj-rest0  32010  bj-inftyexpiinv  32055  bj-inftyexpidisj  32057  taupilem1  32127  f1omptsnlem  32142  mptsnunlem  32144  topdifinffinlem  32154  finixpnum  32347  tan2h  32354  matunitlindflem2  32359  ptrest  32361  poimirlem22  32384  poimirlem25  32387  mblfinlem1  32399  mblfinlem2  32400  mblfinlem3  32401  mblfinlem4  32402  ismblfin  32403  itg2addnclem  32414  itg2addnclem2  32415  itg2addnclem3  32416  itg2addnc  32417  itg2gt0cn  32418  ftc1anclem5  32442  ftc1anclem8  32445  dvasin  32449  dvacos  32450  sdclem2  32491  totbndbnd  32541  heibor1lem  32561  heiborlem7  32569  bfplem1  32574  prnc  32819  riotasv  33046  glbconN  33464  atpointN  33830  polsubN  33994  pol0N  33996  pol1N  33997  2polvalN  34001  2polssN  34002  3polN  34003  pcl0N  34009  2pmaplubN  34013  pnonsingN  34020  polsubclN  34039  cdlemefs32sn1aw  34503  cdleme43fsv1snlem  34509  cdleme41sn3a  34522  cdleme32a  34530  cdleme40m  34556  cdleme40n  34557  cdleme42b  34567  istendo  34849  cdlemk40  35006  cdlemkid  35025  dihvalcqpre  35325  mapfzcons1cl  36082  eldioph3b  36129  eldiophss  36139  0dioph  36143  vdioph  36144  eldioph4b  36176  eldioph4i  36177  rencldnfilem  36185  rmxy1  36288  rmxy0  36289  rmxm1  36300  rmym1  36301  monotoddzzfi  36308  aomclem6  36430  pwslnmlem0  36462  pwslnmlem1  36463  isnumbasabl  36478  areaquad  36604  relexp2  36771  eltrclrec  36774  elrtrclrec  36775  brtrclrec  36790  brrtrclrec  36791  relexpxpmin  36811  dftrcl3  36814  dfrtrcl3  36827  heeq1  36874  seff  37313  lhe4.4ex1a  37333  eelT0  37806  snssl  37870  sineq0ALT  37978  elabrexg  38012  elrnmpt1sf  38154  founiiun0  38155  mapdm0  38161  supxrgere  38273  supxrgelem  38277  fmuldfeqlem1  38432  fmuldfeq  38433  climneg  38460  sumnnodd  38480  addccncf2  38544  dvsinax  38584  stoweidlem18  38694  stoweidlem19  38695  stoweidlem22  38698  stoweidlem34  38710  stoweidlem40  38716  stoweidlem41  38717  stoweidlem55  38731  stoweidlem59  38735  dirker2re  38768  dirkerdenne0  38769  fourierdlem48  38830  fourierdlem49  38831  fourierdlem70  38852  fourierdlem71  38853  fourierdlem104  38886  fourierdlem112  38894  fouriersw  38907  etransclem46  38956  etransclem48  38958  nnfoctbdjlem  39131  rlimdmafv  39690  flsqrt5  39831  bits0ALTV  39912  nnsum3primes4  39988  funop  40124  fsummmodsnunz  40203  upgr0eop  40320  uspgrushgr  40386  usgruspgr  40389  usgr0eop  40453  0grsubgr  40483  dfnbgr2  40542  nbuhgr  40546  uspgrloopvtx  40712  umgr2v2evtx  40718  usgr0edg0rusgr  40756  rgrusgrprc  40770  1wlkvtxiedg  40810  pthdivtx  40916  usgr2pthlem  40950  1wlkpwwlkf1ouspgr  41057  wwlksext2clwwlk  41212  konigsbergssiedgw  41400  frgrncvvdeqlemA  41457  av-numclwwlk2lem1  41513  2zrngnmlid  41720  2zrngnmrid  41721  mpt2exxg2  41890  lco0  41991  zlmodzxzldeplem3  42066  loglt1b  42107  0dig1  42182  aacllem  42298
  Copyright terms: Public domain W3C validator