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

Theorem mpan2 703
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 699 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 196  df-an 385
This theorem is referenced by:  mpanr12  717  mp3an23  1408  eueq2  3347  sbcgf  3468  sbcralg  3480  csbconstgf  3511  sbcnestg  3949  csbnestg  3950  csbnest1g  3953  mpteq1  4665  iinexg  4751  eusv2nf  4790  reusv2lem5  4799  nnullss  4857  xpss1  5151  xpiindi  5179  reldm0  5264  elrnmpt1s  5294  resdm  5361  resid  5379  eliniseg  5413  trinxp  5440  inimasn  5469  ssrnres  5491  cnveq0  5509  coi2  5569  relrelss  5576  cnviin  5589  predep  5623  ord0eln0  5696  funcnvres  5881  funimaex  5890  fnresin1  5919  fnresin2  5920  fresin  5986  dffv3  6099  ssimaex  6173  dmfco  6182  fvmpt  6191  fvmptnf  6210  fvimacnvALT  6244  dff3  6280  fsn  6308  fsn2  6309  funop  6320  fvrnressn  6333  fninfp  6345  fndifnfp  6347  fnnfpeq0  6349  elabrex  6405  f1elima  6421  fsnex  6438  fliftel1  6460  f1owe  6503  sorpssuni  6844  sorpssint  6845  eldifpw  6868  ordeleqon  6880  ordsson  6881  ssnlim  6975  2ndconst  7153  curry1  7156  tposfun  7255  tpostpos2  7260  wfr3g  7300  wfrlem14  7315  wfrlem15  7316  tfrlem10  7370  tfrlem12  7372  tfr3  7382  seqomlem1  7432  seqomlem2  7433  seqomlem4  7435  ondif2  7469  oa0  7483  om0  7484  oa1suc  7498  om1  7509  oe1  7511  oe1m  7512  omass  7547  oeoalem  7563  oeoelem  7565  nnmsucr  7592  nnm1  7615  nnm2  7616  ecelqsg  7689  xpider  7705  qsel  7713  map0e  7781  fvdiagfn  7788  ralxpmap  7793  ixpsnf1o  7834  map1  7921  xp1en  7931  sbthlem7  7961  domunsn  7995  xpmapenlem  8012  infensuc  8023  infi  8069  finresfin  8071  diffi  8077  dif1en  8078  findcard2d  8087  unblem1  8097  unblem2  8098  unblem3  8099  unblem4  8100  isfinite2  8103  infn0  8107  unfilem1  8109  unfilem2  8110  unfir  8113  fofinf1o  8126  cnvfi  8131  pwfilem  8143  mptfi  8148  finsschain  8156  marypha2  8228  eqinf  8273  inf0  8401  trcl  8487  r1rankidb  8550  snwf  8555  unwf  8556  uniwf  8565  rankval3b  8572  rankr1a  8582  rankxplim3  8627  scott0  8632  card1  8677  pm54.43  8709  infxpenc2  8728  dfac8clem  8738  alephsuc2  8786  alephle  8794  cardaleph  8795  dfacacn  8846  dfac13  8847  dfac12lem2  8849  cdaval  8875  uncdadom  8876  cdaun  8877  cdacomen  8886  cdaassen  8887  cdadom1  8891  cdainf  8897  pwcda1  8899  ackbij1lem18  8942  cflem  8951  cflecard  8958  cfeq0  8961  cfslb  8971  cfsmolem  8975  cfcoflem  8977  cfidm  8980  isfin4-3  9020  fin23lem12  9036  fin23lem16  9040  fin23lem28  9045  fin23lem38  9054  fin23lem41  9057  fin1a2lem7  9111  fin1a2lem12  9116  fin1a2lem13  9117  hsmexlem8  9129  axcc2lem  9141  axcc3  9143  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  ac6num  9184  ttukeylem4  9217  ttukeylem7  9220  ttukey2g  9221  axdclem  9224  brdom3  9231  brdom5  9232  cardeq0  9253  unsnen  9254  konigthlem  9269  pwcfsdom  9284  canthp1lem1  9353  wunex2  9439  wuncval2  9448  eltsk2g  9452  intgru  9515  ingru  9516  grutsk  9523  axgroth6  9529  mulidpi  9587  nlt1pi  9607  indpi  9608  pinq  9628  mulidnq  9664  1idpr  9730  prlem934  9734  0idsr  9797  1idsr  9798  00sr  9799  negexsr  9802  recexsrlem  9803  sqgt0sr  9806  ax1rid  9861  axcnre  9864  ne0gt0  10021  peano2cn  10087  peano2re  10088  00id  10090  mul02lem2  10092  mul01  10094  subid  10179  subid1  10180  negid  10207  negeq0  10214  peano2cnm  10226  peano2rem  10227  lt0neg1  10413  le0neg1  10415  relin01  10431  div2neg  10627  recgt0ii  10808  divgt0i2i  10818  ledivp1i  10828  ltdivp1i  10829  peano5nni  10900  peano2nn  10909  nnge1  10923  times2  11023  addltmul  11145  nn0p1nn  11209  peano2nn0  11210  nn0lele2xi  11225  frnnn0fsupp  11227  peano2z  11295  peano2zm  11297  suprzcl  11333  zeo  11339  uzwo  11627  uzwo2  11628  infssuzle  11647  infssuzcl  11648  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  rphalfcl  11734  zgt1rpn0n1  11747  ltpnf  11830  nltmnf  11839  pnfge  11840  nltpnft  11871  qsqueeze  11906  xlt0neg1  11924  xle0neg1  11926  xaddpnf1  11931  xaddmnf1  11933  xaddid1  11946  xsubge0  11963  xmul01  11969  xmulneg1  11971  xmulpnf1  11976  xmulid1  11981  supxrbnd  12030  supxrgtmnf  12031  supxrre1  12032  supxrre2  12033  elioopnf  12138  elicopnf  12140  xrge0neqmnf  12147  iccshftri  12178  iccshftli  12180  iccdili  12182  icccntri  12184  fzprval  12271  fzofzp1  12431  fzostep1  12446  injresinj  12451  flge0nn0  12483  flge1nn  12484  btwnzge0  12491  modfrac  12545  om2uzsuci  12609  axdc4uzlem  12644  ser1const  12719  exp0  12726  exp1  12728  expn1  12732  nn0sqcl  12749  expubnd  12783  sqval  12784  sqeq0  12789  resqcl  12793  zsqcl  12796  binom21  12842  expnbnd  12855  nn0opthlem2  12918  bcnn  12961  bcn2  12968  bcn2p1  12974  bcnm1  12976  hasheq0  13015  hashsng  13020  hashen1  13021  hashin  13060  hashdif  13062  hashxplem  13080  hashf1lem2  13097  hash2pr  13108  hash2prde  13109  pr2pwpr  13116  hash3tr  13127  iswrd  13162  wrdval  13163  wrdv  13175  ccatval2  13215  ccatrid  13223  s111  13248  swrd0len0  13288  repsw0  13375  repsw1  13381  cshw0  13391  wwlktovf  13547  relexpsucnnl  13620  shftfib  13660  reim0  13706  imval2  13739  cjne0  13751  abssq  13894  max0add  13898  abs2dif  13920  rddif  13928  absrdbnd  13929  rexuz3  13936  rlimdm  14130  isershft  14242  isercolllem2  14244  isercoll  14246  fsum  14298  fsumadd  14317  fsumsplitsnun  14328  bcxmas  14406  infcvgaux2i  14429  fprod  14510  risefac0  14597  fallfac0  14598  risefac1  14603  fallfac1  14604  bpoly2  14627  bpoly3  14628  bpoly4  14629  fsumcube  14630  efi4p  14706  resin4p  14707  recos4p  14708  sinbnd  14749  cosbnd  14750  znnenlem  14779  rpnnen2lem8  14789  rpnnen2lem12  14793  cnso  14815  dvdsmul2  14842  dvdslelem  14869  odd2np1lem  14902  mod2eq1n2dvds  14909  divalglem0  14954  divalglem1  14955  divalglem4  14957  divalglem5  14958  divalglem8  14961  flodddiv4  14975  bits0  14988  bitsp1o  14993  bitsf1  15006  sadadd2lem2  15010  gcd1  15087  gcdmultiple  15107  lcm0val  15145  dvdslcm  15149  lcmeq0  15151  lcmgcd  15158  lcm1  15161  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  prm2orodd  15242  phiprm  15320  pc0  15397  pcdvdstr  15418  vdwlem2  15524  vdwlem6  15528  vdwlem8  15530  hashbc0  15547  setsval  15720  fsets  15723  setsres  15729  ressinbas  15763  ressress  15765  elrestr  15912  pwssnf1o  15981  xpsfrnel  16046  ismred2  16086  submre  16088  mreacs  16142  oppchomfval  16197  brssc  16297  isssc  16303  yonedalem4c  16740  isprs  16753  oduleval  16954  oduclatb  16967  gsumval2a  17102  mulg1  17371  mulgnegnn  17374  isghm  17483  ghmghmrn  17502  cntrnsg  17597  oppgplusfval  17601  psgneldm2i  17748  efgrelexlemb  17986  frgp0  17996  frgpmhm  18001  vrgpf  18004  cygctb  18116  dprd0  18253  dprd2da  18264  mgpplusg  18316  opprmulfval  18448  subrgint  18625  lsp0  18830  sralem  18998  rlmval2  19015  fczpsrbag  19188  ply1idvr1  19484  evls1rhmlem  19507  evl1fval1lem  19515  zringcyg  19658  mulgrhm2  19666  zlmsca  19688  chrnzr  19697  zrhpsgnelbas  19759  ocvz  19841  cssincl  19851  css0  19852  css1  19853  frlmip  19936  mat1scmat  20164  marrepeval  20188  decpmatid  20394  0opn  20534  topopn  20536  basdif0  20568  tgval  20570  isopn2  20646  0cld  20652  ntropn  20663  ntrval2  20665  ntrdif  20666  clsdif  20667  cmclsopn  20676  clstop  20683  ntrtop  20684  cls0  20694  ntr0  20695  mretopd  20706  neips  20727  neiptopnei  20746  maxlp  20761  isperf2  20766  rest0  20783  iocpnfordt  20829  icomnfordt  20830  mnfnei  20835  refref  21126  unisngl  21140  1stckgen  21167  ptbasfi  21194  pthaus  21251  imasnopn  21303  imasncld  21304  imasncls  21305  fbssfi  21451  isfil2  21470  ssfg  21486  filcon  21497  fbasrn  21498  filufint  21534  imaelfm  21565  fmfnfmlem4  21571  fclsfnflim  21641  alexsubALTlem3  21663  alexsubALTlem4  21664  ustfilxp  21826  ustuqtop1  21855  ustuqtop2  21856  ustuqtop3  21857  ustuqtop4  21858  utopsnneiplem  21861  utopsnnei  21863  utop2nei  21864  cfiluweak  21909  neipcfilu  21910  xmetres  21979  metres  21980  mopnex  22134  prdsms  22146  blval2  22177  metucn  22186  tngds  22262  tngngp3  22270  nmoge0  22335  cnfldnm  22392  tgioo  22407  xrtgioo  22417  xrsmopn  22423  negcncf  22529  phtpy01  22592  pco0  22622  tchtopn  22833  tchnmfval  22835  caussi  22903  rrxip  22986  minveclem3b  23007  ovolfioo  23043  ovolficc  23044  ovolfsf  23047  ovolctb  23065  ovolctb2  23067  ovolfiniun  23076  ovoliun2  23081  ovolshftlem1  23084  ovolscalem1  23088  ovolicopnf  23099  iunmbl2  23132  uniioombllem2  23157  opnmblALT  23177  ismbf  23203  mbfinf  23238  0plef  23245  itg1climres  23287  itg2cnlem1  23334  iblitg  23341  ibl0  23359  itgcn  23415  cnlimc  23458  dvfre  23520  dvnfre  23521  dveflem  23546  dvef  23547  dvlipcn  23561  lhop2  23582  itgsubstlem  23615  deg1val  23660  ply1rem  23727  coefv0  23808  plyrecj  23839  vieta1lem2  23870  aannenlem1  23887  aaliou2b  23900  ulmval  23938  ulmpm  23941  ulmdvlem1  23958  mtest  23962  efcn  24001  sin2pim  24041  cos2pim  24042  sinmpi  24043  cosmpi  24044  sinppi  24045  cosppi  24046  efimpi  24047  sincosq1lem  24053  sincosq2sgn  24055  sincosq3sgn  24056  sincosq4sgn  24057  sinq12gt0  24063  sinq34lt0t  24065  sincosq1eq  24068  abssinper  24074  efif1o  24096  relogcn  24184  ellogdm  24185  efopn  24204  cxp0  24216  cxp1  24217  cxpsqrt  24249  logsqrt  24250  logb1  24307  atandm3  24405  atanbnd  24453  atancn  24463  leibpi  24469  efrlim  24496  logdifbnd  24520  vmaprm  24643  ppip1le  24687  ppieq0  24702  prmorcht  24704  ppiublem1  24727  ppiub  24729  chpeq0  24733  chtub  24737  fsumvma  24738  pclogsum  24740  chpval2  24743  dchrresb  24784  dchrptlem1  24789  lgs0  24835  lgs2  24839  lgsdir2lem2  24851  lgsdir2lem4  24853  lgsdchrval  24879  lgsdchr  24880  lgseisenlem2  24901  2lgslem1c  24918  2lgsoddprmlem2  24934  dirith2  25017  selberg2lem  25039  qabvle  25114  qabvexp  25115  ostth  25128  istrkg2ld  25159  ttgval  25555  cchhllem  25567  brbtwn  25579  colinearalglem4  25589  upgr0eop  25780  uhgra0  25838  umgra0  25854  umisuhgra  25856  uslisushgra  25892  usisuslgra  25894  usgra0  25899  usgraedg4  25916  usgrafisbase  25943  usgrasscusgra  26011  uvtx01vtx  26020  usgra2adedgwlkonALT  26144  usgra2wlkspthlem2  26148  fargshiftlem  26162  usgrcyclnl2  26169  constr3trl  26187  constr3pth  26188  constr3cycl  26189  4cycl4dv  26195  wwlkn0s  26233  el2wlkonotlem  26389  usg2wlkonot  26410  usg2wotspth  26411  iseupa  26492  frgrancvvdeqlemA  26564  ex-po  26684  nvnd  26927  ipval2lem3  26944  ipval2  26946  ipidsq  26949  dipcj  26953  dip0r  26956  nmlnogt0  27036  blocni  27044  ipasslem2  27071  ipasslem8  27076  ipasslem9  27077  ajval  27101  ubthlem1  27110  hvaddid2  27264  hvsub0  27317  hi02  27338  hlimi  27429  isch2  27464  chlimi  27475  chsupunss  27587  shsupunss  27589  chlejb1i  27719  h1dei  27793  h1de2ci  27799  spanunsni  27822  pjoml2i  27828  pjorthi  27912  mayete3i  27971  hosubid1  28041  nmopge0  28154  nmfnge0  28170  adj1  28176  adjeq  28178  lnop0  28209  lnopmi  28243  nmophmi  28274  cnlnadjlem5  28314  cnlnadjeui  28320  unierri  28347  leoprf2  28370  leopnmid  28381  nmopleid  28382  hstles  28474  hst0  28476  strlem3a  28495  dmdbr2  28546  mdsl1i  28564  mdsl2i  28565  mdsl2bi  28566  cvmdi  28567  mdslmd1lem1  28568  mdslmd1lem2  28569  mdslmd1i  28572  mdslmd2i  28573  csmdsymi  28577  mdexchi  28578  superpos  28597  atomli  28625  atordi  28627  chirredlem1  28633  chirredlem2  28634  atcvat4i  28640  atabsi  28644  mdsymlem1  28646  mdsymlem5  28650  mdsymlem6  28651  sumdmdii  28658  dmdbr5ati  28665  dmdbr6ati  28666  mddmdin0i  28674  cdj3lem2  28678  xppreima  28829  abfmpunirn  28832  abfmpel  28835  aciunf1lem  28844  fgreu  28854  imafi2  28872  padct  28885  fpwrelmapffslem  28895  fpwrelmap  28896  xlemnf  28905  xrge0infss  28915  xrdifh  28932  clatp0cl  29002  clatp1cl  29003  resvval  29158  rearchi  29173  locfinreflem  29235  locfinref  29236  ordtconlem1  29298  rge0scvg  29323  lmxrge0  29326  qqh0  29356  qqh1  29357  rrh0  29387  zrhre  29391  esumcst  29452  esumfzf  29458  esumfsupre  29460  hasheuni  29474  sgon  29514  dmvlsiga  29519  sigainb  29526  measval  29588  ismeas  29589  sxbrsigalem0  29660  omssubadd  29689  carsggect  29707  eulerpartlemmf  29764  eulerpartlemgs2  29769  eulerpartlemn  29770  rrvsum  29843  ballotlem2  29877  ballotlemfcc  29882  ballotlem4  29887  signsplypnf  29953  signsply0  29954  signsw0glem  29956  signswrid  29961  signlem0  29990  bnj535  30214  bnj580  30237  bnj907  30289  bnj1253  30339  ptpcon  30469  cvmsss2  30510  cvmlift2lem12  30550  cvmlift2lem13  30551  cvmliftphtlem  30553  cvmliftpht  30554  mppsthm  30730  bcneg1  30875  fprb  30916  opelco3  30923  fv1stcnv  30925  fv2ndcnv  30926  trpred0  30980  wlimeq1  31010  frr3g  31023  noxpsgn  31062  funpartfv  31222  imagesset  31230  altopeq1  31240  brcolinear2  31335  gtinfOLD  31484  cldbnd  31491  ivthALT  31500  refssfne  31523  tailfb  31542  ontgval  31600  onint1  31618  axc11n11r  31860  bj-restsn10  32220  bj-restsnid  32221  bj-rest10  32222  bj-rest0  32227  bj-inftyexpiinv  32272  bj-inftyexpidisj  32274  taupilem1  32344  f1omptsnlem  32359  mptsnunlem  32361  topdifinffinlem  32371  finixpnum  32564  tan2h  32571  matunitlindflem2  32576  ptrest  32578  poimirlem22  32601  poimirlem25  32604  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  ftc1anclem5  32659  ftc1anclem8  32662  dvasin  32666  dvacos  32667  sdclem2  32708  totbndbnd  32758  heibor1lem  32778  heiborlem7  32786  bfplem1  32791  prnc  33036  riotasv  33263  glbconN  33681  atpointN  34047  polsubN  34211  pol0N  34213  pol1N  34214  2polvalN  34218  2polssN  34219  3polN  34220  pcl0N  34226  2pmaplubN  34230  pnonsingN  34237  polsubclN  34256  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdleme41sn3a  34739  cdleme32a  34747  cdleme40m  34773  cdleme40n  34774  cdleme42b  34784  istendo  35066  cdlemk40  35223  cdlemkid  35242  dihvalcqpre  35542  mapfzcons1cl  36299  eldioph3b  36346  eldiophss  36356  0dioph  36360  vdioph  36361  eldioph4b  36393  eldioph4i  36394  rencldnfilem  36402  rmxy1  36505  rmxy0  36506  rmxm1  36517  rmym1  36518  monotoddzzfi  36525  aomclem6  36647  pwslnmlem0  36679  pwslnmlem1  36680  isnumbasabl  36695  areaquad  36821  relexp2  36988  eltrclrec  36991  elrtrclrec  36992  brtrclrec  37007  brrtrclrec  37008  relexpxpmin  37028  dftrcl3  37031  dfrtrcl3  37044  heeq1  37091  seff  37530  lhe4.4ex1a  37550  eelT0  38023  snssl  38087  sineq0ALT  38195  elabrexg  38229  elrnmpt1sf  38371  founiiun0  38372  mapdm0  38378  supxrgere  38490  supxrgelem  38494  fmuldfeqlem1  38649  fmuldfeq  38650  climneg  38677  sumnnodd  38697  addccncf2  38761  dvsinax  38801  stoweidlem18  38911  stoweidlem19  38912  stoweidlem22  38915  stoweidlem34  38927  stoweidlem40  38933  stoweidlem41  38934  stoweidlem55  38948  stoweidlem59  38952  dirker2re  38985  dirkerdenne0  38986  fourierdlem48  39047  fourierdlem49  39048  fourierdlem70  39069  fourierdlem71  39070  fourierdlem104  39103  fourierdlem112  39111  fouriersw  39124  etransclem46  39173  etransclem48  39175  nnfoctbdjlem  39348  rlimdmafv  39906  flsqrt5  40047  bits0ALTV  40128  nnsum3primes4  40204  fsummmodsnunz  40374  uspgrushgr  40405  usgruspgr  40408  usgr0eop  40472  0grsubgr  40502  dfnbgr2  40561  nbuhgr  40565  uspgrloopvtx  40731  umgr2v2evtx  40737  usgr0edg0rusgr  40775  rgrusgrprc  40789  1wlkvtxiedg  40829  pthdivtx  40935  usgr2pthlem  40969  1wlkpwwlkf1ouspgr  41076  wwlksext2clwwlk  41231  konigsbergssiedgw  41419  frgrncvvdeqlemA  41476  av-numclwwlk2lem1  41532  2zrngnmlid  41739  2zrngnmrid  41740  mpt2exxg2  41909  lco0  42010  zlmodzxzldeplem3  42085  loglt1b  42126  0dig1  42201  aacllem  42356
  Copyright terms: Public domain W3C validator