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

Theorem mpan2 687
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 683 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mpanr12  701  mp3an23  1444  elvd  3501  eueq2  3700  sbcgf  3844  sbcralg  3856  csbconstgf  3900  sbcnestgw  4371  csbnestgw  4372  sbcnestg  4376  csbnestg  4377  csbnest1g  4380  mpteq1  5146  iinexg  5236  eusv2nf  5287  reusv2lem5  5294  nnullss  5346  xpss1  5568  xpiindi  5700  reldm0  5792  elrnmpt1s  5823  resdm  5891  eliniseg  5952  trinxp  5979  ssrnres  6029  cnveq0  6048  coi2  6110  relrelss  6118  cnviin  6131  ord0eln0  6239  funcnvres  6426  funimaex  6435  fnresin1  6466  fnresin2  6467  fresin  6541  ssimaex  6742  fvmpt  6762  fvmptnf  6783  fvimacnvALT  6820  dff3  6859  fsn  6890  fsn2  6891  funop  6904  fvrnressn  6916  fninfp  6929  fndifnfp  6931  fnnfpeq0  6933  fprb  6949  elabrex  6993  f1elima  7012  fliftel1  7052  f1owe  7095  sorpssuni  7447  sorpssint  7448  eldifpw  7478  ordeleqon  7491  ordsson  7492  ssnlim  7587  tposfun  7899  tpostpos2  7904  wfr3g  7944  wfrlem14  7959  wfrlem15  7960  tfrlem10  8014  tfrlem12  8016  tfr3  8026  seqomlem1  8077  seqomlem2  8078  seqomlem4  8080  ondif2  8118  oa0  8132  om0  8133  oa1suc  8147  om1  8158  oe1  8160  oe1m  8161  omass  8196  oeoalem  8212  oeoelem  8214  nnmsucr  8241  nnm1  8265  nnm2  8266  ecelqsg  8342  xpider  8358  mapdm0  8411  fvdiagfn  8444  ixpsnf1o  8491  xp1en  8592  sbthlem7  8622  domunsn  8656  xpmapenlem  8673  infensuc  8684  infi  8731  finresfin  8733  diffi  8739  findcard2d  8749  unblem1  8759  unblem2  8760  unblem3  8761  unblem4  8762  isfinite2  8765  infn0  8769  unfilem1  8771  unfilem2  8772  unfir  8775  fofinf1o  8788  cnvfi  8795  pwfilem  8807  mptfi  8812  finsschain  8820  marypha2  8892  inf0  9073  trcl  9159  r1rankidb  9222  snwf  9227  unwf  9228  uniwf  9237  rankval3b  9244  rankr1a  9254  rankxplim3  9299  scott0  9304  djueq1  9323  card1  9386  pm54.43  9418  infxpenc2  9437  dfac8clem  9447  alephsuc2  9495  alephle  9503  cardaleph  9504  dfac12lem2  9559  undjudom  9582  djudom1  9597  pwdju1  9605  ackbij1lem18  9648  cflem  9657  cflecard  9664  cfeq0  9667  cfslb  9677  cfsmolem  9681  cfcoflem  9683  cfidm  9686  isfin4p1  9726  fin23lem12  9742  fin23lem16  9746  fin23lem28  9751  fin23lem38  9760  fin23lem41  9763  fin1a2lem7  9817  fin1a2lem12  9822  fin1a2lem13  9823  hsmexlem8  9835  axcc2lem  9847  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  axcclem  9868  ac6num  9890  ttukeylem4  9923  ttukeylem7  9926  ttukey2g  9927  axdclem  9930  brdom3  9939  brdom5  9940  cardeq0  9963  unsnen  9964  konigthlem  9979  pwcfsdom  9994  canthp1lem1  10063  wunex2  10149  wuncval2  10158  eltsk2g  10162  ingru  10226  grutsk  10233  axgroth6  10239  mulidpi  10297  nlt1pi  10317  indpi  10318  pinq  10338  mulidnq  10374  1idpr  10440  prlem934  10444  0idsr  10508  1idsr  10509  00sr  10510  negexsr  10513  recexsrlem  10514  sqgt0sr  10517  ax1rid  10572  axcnre  10575  ne0gt0  10734  peano2cn  10801  peano2re  10802  00id  10804  mul02lem2  10806  mul01  10808  subid  10894  subid1  10895  negid  10922  negeq0  10929  peano2cnm  10941  peano2rem  10942  lt0neg1  11135  le0neg1  11137  relin01  11153  div2neg  11352  recgt0ii  11535  divgt0i2i  11544  ledivp1i  11554  ltdivp1i  11555  peano5nni  11630  peano2nn  11639  nnge1  11654  times2  11763  addltmul  11862  nn0p1nn  11925  peano2nn0  11926  nn0lele2xi  11941  frnnn0fsupp  11943  peano2z  12012  peano2zm  12014  suprzcl  12051  zeo  12057  uzwo  12300  uzwo2  12301  infssuzle  12320  infssuzcl  12321  zq  12343  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  rphalfcl  12406  zgt1rpn0n1  12420  ltpnf  12505  nltmnf  12514  pnfge  12515  nltpnft  12547  xlemnf  12550  qsqueeze  12584  xlt0neg1  12602  xle0neg1  12604  xaddpnf1  12609  xaddmnf1  12611  xaddid1  12624  xsubge0  12644  xmul01  12650  xmulneg1  12652  xmulpnf1  12657  xmulid1  12662  supxrbnd  12711  supxrgtmnf  12712  supxrre1  12713  supxrre2  12714  elioopnf  12821  elicopnf  12823  iccshftri  12863  iccshftli  12865  iccdili  12867  icccntri  12869  fzprval  12958  fz0add1fz1  13097  fzofzp1  13124  fzostep1  13143  injresinj  13148  flge0nn0  13180  flge1nn  13181  btwnzge0  13188  modfrac  13242  om2uzsuci  13306  axdc4uzlem  13341  ser1const  13416  exp0  13423  exp1  13425  expn1  13429  nn0sqcl  13446  sqval  13471  sqeq0  13476  resqcl  13480  zsqcl  13484  expubnd  13531  binom21  13570  expnbnd  13583  nn0opthlem2  13619  bcnn  13662  bcn2  13669  bcn2p1  13675  bcnm1  13677  hasheq0  13714  hashsng  13720  hashen1  13721  hashunsnggt  13745  hashin  13762  hashdif  13764  hashgt23el  13775  hashxplem  13784  hashf1lem2  13804  hash2pr  13817  hash2prde  13818  pr2pwpr  13827  hash3tr  13838  iswrd  13853  wrdval  13854  wrdvOLD  13868  hashwrdn  13888  ccatval2  13922  ccatrid  13931  eqs1  13956  s111  13959  ccatws1len  13964  repsw0  14129  repsw1  14135  cshw0  14146  wwlktovf  14310  relexpsucnnl  14381  reim0  14467  imval2  14500  cjne0  14512  abssq  14656  max0add  14660  abs2dif  14682  rddif  14690  absrdbnd  14691  rexuz3  14698  isershft  15010  isercolllem2  15012  isercoll  15014  fsum  15067  fsumadd  15086  fsumsplitsnun  15100  bcxmas  15180  infcvgaux2i  15203  fprod  15285  risefac0  15371  fallfac0  15372  risefac1  15377  fallfac1  15378  bpoly2  15401  bpoly3  15402  bpoly4  15403  fsumcube  15404  efi4p  15480  resin4p  15481  recos4p  15482  sinbnd  15523  cosbnd  15524  rpnnen2lem8  15564  rpnnen2lem12  15568  cnso  15590  dvdsmul2  15622  dvdslelem  15649  odd2np1lem  15679  mod2eq1n2dvds  15686  divalglem0  15734  divalglem1  15735  divalglem4  15737  divalglem5  15738  divalglem8  15741  flodddiv4  15754  bits0  15767  bitsp1o  15772  bitsf1  15785  sadadd2lem2  15789  gcd1  15866  gcdmultipleOLD  15890  lcm0val  15928  dvdslcm  15932  lcmeq0  15934  lcmgcd  15941  lcm1  15944  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  prm2orodd  16025  phiprm  16104  pc0  16181  pcdvdstr  16202  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  hashbc0  16331  setsval  16503  fsets  16506  setsres  16515  ressinbas  16550  ressress  16552  elrestr  16692  pwssnf1o  16761  xpsfrnel  16825  xpscf  16828  ismred2  16864  submre  16866  mreacs  16919  oppchomfval  16974  brssc  17074  isssc  17080  yonedalem4c  17517  isprs  17530  oduleval  17731  oduclatb  17744  gsumval2a  17885  mulg1  18175  mulgnegnn  18178  isghm  18298  ghmghmrn  18317  cntrnsg  18412  oppgplusfval  18416  psgneldm2i  18564  efgrelexlemb  18807  frgp0  18817  frgpmhm  18822  vrgpf  18825  cntrcmnd  18893  cntrabl  18894  cygctb  18943  dprd0  19084  dprd2da  19095  mgpplusg  19174  opprmulfval  19306  subrgint  19488  lsp0  19712  sralem  19880  rlmval2  19897  fczpsrbag  20077  ply1idvr1  20391  evls1rhmlem  20414  evl1fval1lem  20423  zringcyg  20568  mulgrhm2  20576  zlmsca  20598  chrnzr  20607  zrhpsgnelbas  20668  ocvz  20752  cssincl  20762  css0  20763  css1  20764  frlmip  20852  marrepeval  21102  decpmatid  21308  0opn  21442  topopn  21444  basdif0  21491  tgval  21493  isopn2  21570  0cld  21576  ntropn  21587  ntrval2  21589  ntrdif  21590  clsdif  21591  cmclsopn  21600  ntrtop  21608  ntr0  21619  mretopd  21630  neips  21651  neiptopnei  21670  maxlp  21685  isperf2  21690  rest0  21707  iocpnfordt  21753  icomnfordt  21754  mnfnei  21759  refref  22051  unisngl  22065  1stckgen  22092  ptbasfi  22119  pthaus  22176  fbssfi  22375  isfil2  22394  ssfg  22410  filconn  22421  fbasrn  22422  filufint  22458  imaelfm  22489  fmfnfmlem4  22495  fclsfnflim  22565  alexsubALTlem3  22587  alexsubALTlem4  22588  ustfilxp  22750  ustuqtop2  22780  ustuqtop4  22782  utopsnneiplem  22785  utopsnnei  22787  utop2nei  22788  cfiluweak  22833  neipcfilu  22834  xmetres  22903  metres  22904  mopnex  23058  prdsms  23070  metucn  23110  tngds  23186  tngngp3  23194  nmoge0  23259  cnfldnm  23316  tgioo  23333  xrtgioo  23343  xrsmopn  23349  negcncf  23455  phtpy01  23518  pco0  23547  tcphtopn  23758  tchnmfval  23760  caussi  23829  rrxip  23922  minveclem3b  23960  ovolfioo  23997  ovolficc  23998  ovolfsf  24001  ovolctb  24020  ovolctb2  24022  ovolfiniun  24031  ovoliun2  24036  ovolshftlem1  24039  ovolscalem1  24043  ovolicopnf  24054  iunmbl2  24087  uniioombllem2  24113  opnmblALT  24133  ismbf  24158  mbfinf  24195  0plef  24202  itg1climres  24244  itg2cnlem1  24291  iblitg  24298  ibl0  24316  itgcn  24372  cnlimc  24415  dvfre  24477  dvnfre  24478  dveflem  24505  dvef  24506  dvlipcn  24520  lhop2  24541  itgsubstlem  24574  deg1val  24619  ply1rem  24686  coefv0  24767  plyrecj  24798  vieta1lem2  24829  aannenlem1  24846  aaliou2b  24859  ulmval  24897  ulmpm  24900  ulmdvlem1  24917  mtest  24921  efcn  24960  sin2pim  25000  cos2pim  25001  sinmpi  25002  cosmpi  25003  sinppi  25004  cosppi  25005  efimpi  25006  sincosq1lem  25012  sincosq2sgn  25014  sincosq3sgn  25015  sincosq4sgn  25016  sinq12gt0  25022  sinq34lt0t  25024  sincosq1eq  25027  abssinper  25035  efif1o  25057  loglt1b  25144  relogcn  25148  ellogdm  25149  efopn  25168  cxp0  25180  cxp1  25181  cxpsqrt  25213  logsqrt  25214  logb1  25274  atandm3  25383  atanbnd  25431  atancn  25441  leibpi  25448  efrlim  25475  logdifbnd  25499  vmaprm  25622  ppip1le  25666  ppieq0  25681  prmorcht  25683  ppiublem1  25706  ppiub  25708  chpeq0  25712  chtub  25716  fsumvma  25717  pclogsum  25719  chpval2  25722  dchrresb  25763  dchrptlem1  25768  lgs0  25814  lgs2  25818  lgsdir2lem2  25830  lgsdir2lem4  25832  lgsdchrval  25858  lgsdchr  25859  lgseisenlem2  25880  2lgslem1c  25897  2lgsoddprmlem2  25913  addsq2nreurex  25948  dirith2  26032  selberg2lem  26054  qabvle  26129  qabvexp  26130  ostth  26143  istrkg2ld  26174  istrkg3ld  26175  ttgval  26589  cchhllem  26601  brbtwn  26613  colinearalglem4  26623  upgr0eop  26827  uspgrushgr  26888  usgruspgr  26891  usgr0eop  26956  0grsubgr  26988  uspgrloopvtx  27225  umgr2v2evtx  27231  usgr0edg0rusgr  27285  rgrusgrprc  27299  wlkvtxiedg  27334  pthdivtx  27438  usgr2pthlem  27472  wlkswwlksf1o  27585  wwlksext2clwwlk  27764  konigsbergssiedgw  27957  frgrncvvdeqlem7  28012  2clwwlk2  28055  ex-po  28142  pliguhgr  28191  nvnd  28393  ipval2lem3  28410  ipval2  28412  ipidsq  28415  dipcj  28419  dip0r  28422  nmlnogt0  28502  blocni  28510  ipasslem2  28537  ipasslem8  28542  ipasslem9  28543  ajval  28566  ubthlem1  28575  hvaddid2  28728  hvsub0  28781  hi02  28802  hlimi  28893  isch2  28928  chlimi  28939  chsupunss  29049  shsupunss  29051  chlejb1i  29181  h1dei  29255  h1de2ci  29261  spanunsni  29284  pjoml2i  29290  pjorthi  29374  mayete3i  29433  hosubid1  29503  nmopge0  29616  nmfnge0  29632  adj1  29638  adjeq  29640  lnop0  29671  lnopmi  29705  nmophmi  29736  cnlnadjlem5  29776  cnlnadjeui  29782  unierri  29809  leoprf2  29832  leopnmid  29843  nmopleid  29844  hstles  29936  hst0  29938  strlem3a  29957  dmdbr2  30008  mdsl1i  30026  mdsl2i  30027  mdsl2bi  30028  cvmdi  30029  mdslmd1lem1  30030  mdslmd1lem2  30031  mdslmd1i  30034  mdslmd2i  30035  csmdsymi  30039  mdexchi  30040  superpos  30059  atomli  30087  atordi  30089  chirredlem1  30095  chirredlem2  30096  atcvat4i  30102  atabsi  30106  mdsymlem1  30108  mdsymlem5  30112  mdsymlem6  30113  sumdmdii  30120  dmdbr5ati  30127  dmdbr6ati  30128  mddmdin0i  30136  cdj3lem2  30140  unidifsnel  30223  unidifsnne  30224  xppreima  30323  abfmpunirn  30326  abfmpel  30329  aciunf1lem  30336  fgreu  30346  imafi2  30374  padct  30382  fpwrelmapffslem  30395  fpwrelmap  30396  xrge0infss  30411  xrdifh  30430  pfx1s2  30543  clatp0cl  30586  clatp1cl  30587  cntrcrng  30625  cycpmco2lem4  30699  rmfsupp2  30794  resvval  30828  rearchi  30843  qusxpid  30856  locfinreflem  31004  locfinref  31005  ordtconnlem1  31067  rge0scvg  31092  lmxrge0  31095  qqh0  31125  qqh1  31126  rrh0  31156  zrhre  31160  esumcst  31222  esumfzf  31228  esumfsupre  31230  hasheuni  31244  sgon  31283  dmvlsiga  31288  sigainb  31295  measval  31357  ismeas  31358  sxbrsigalem0  31429  omssubadd  31458  carsggect  31476  eulerpartlemmf  31533  eulerpartlemgs2  31538  eulerpartlemn  31539  rrvsum  31612  ballotlem2  31646  ballotlemfcc  31651  ballotlem4  31656  signsplypnf  31720  signsply0  31721  signsw0glem  31723  signswrid  31728  signlem0  31757  signshf  31758  bnj535  32062  bnj580  32085  bnj907  32137  bnj1253  32187  funen1cnv  32255  loop1cycl  32282  ptpconn  32378  cvmsss2  32419  cvmlift2lem12  32459  cvmlift2lem13  32460  cvmliftphtlem  32462  cvmliftpht  32463  fmlafvel  32530  mppsthm  32724  bcneg1  32866  fv1stcnv  32918  fv2ndcnv  32919  trpred0  32973  wlimeq1  33005  frr3g  33019  fpr3g  33020  noextendseq  33072  noetalem3  33117  scutun12  33169  imagesset  33312  altopeq1  33322  brcolinear2  33417  cldbnd  33572  ivthALT  33581  refssfne  33604  ontgval  33677  onint1  33695  axc11n11r  33915  bj-bm1.3ii  34252  bj-restsn0  34271  bj-restsn10  34272  bj-restsnid  34273  bj-rest10  34274  bj-rest0  34279  bj-inftyexpiinv  34383  bj-inftyexpidisj  34385  taupilem1  34485  f1omptsnlem  34500  mptsnunlem  34502  topdifinffinlem  34511  inunissunidif  34539  rdgssun  34542  exrecfnlem  34543  exrecfnpw  34545  finixpnum  34759  tan2h  34766  matunitlindflem2  34771  ptrest  34773  poimirlem22  34796  poimirlem25  34799  mblfinlem1  34811  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  itg2addnclem  34825  itg2addnclem2  34826  itg2addnclem3  34827  itg2addnc  34828  itg2gt0cn  34829  ftc1anclem5  34853  ftc1anclem8  34856  dvasin  34860  dvacos  34861  sdclem2  34900  totbndbnd  34950  heibor1lem  34970  heiborlem7  34978  bfplem1  34983  prnc  35228  ecexALTV  35471  brxrn  35508  riotasv  35977  glbconN  36395  atpointN  36761  polsubN  36925  pol0N  36927  pol1N  36928  2polvalN  36932  2polssN  36933  3polN  36934  pcl0N  36940  2pmaplubN  36944  pnonsingN  36951  polsubclN  36970  cdlemefs32sn1aw  37432  cdleme43fsv1snlem  37438  cdleme41sn3a  37451  cdleme32a  37459  cdleme40m  37485  cdleme40n  37486  cdleme42b  37496  istendo  37778  cdlemk40  37935  cdlemkid  37954  dihvalcqpre  38253  fnsnbt  39000  frlmsnic  39029  0prjspn  39150  3cubes  39167  mapfzcons1cl  39195  eldioph3b  39242  eldiophss  39251  0dioph  39255  vdioph  39256  eldioph4b  39288  eldioph4i  39289  rencldnfilem  39297  rmxy1  39399  rmxy0  39400  rmxm1  39411  rmym1  39412  monotoddzzfi  39419  aomclem6  39539  pwslnmlem0  39571  isnumbasabl  39586  areaquad  39703  relexp2  39902  eltrclrec  39905  elrtrclrec  39906  brtrclrec  39921  brrtrclrec  39922  relexpxpmin  39942  dftrcl3  39945  dfrtrcl3  39958  heeq1  40003  seff  40521  lhe4.4ex1a  40541  eelT0  40989  snssl  41044  sineq0ALT  41151  elabrexg  41183  elrnmpt1sf  41330  founiiun0  41331  supxrgere  41481  supxrgelem  41485  fmuldfeqlem1  41743  fmuldfeq  41744  climneg  41771  sumnnodd  41791  liminfltlem  41965  xlimpnfxnegmnf2  42019  addccncf2  42039  dvsinax  42077  stoweidlem18  42184  stoweidlem19  42185  stoweidlem22  42188  stoweidlem34  42200  stoweidlem40  42206  stoweidlem41  42207  stoweidlem55  42221  stoweidlem59  42225  dirker2re  42258  dirkerdenne0  42259  fourierdlem48  42320  fourierdlem49  42321  fourierdlem70  42342  fourierdlem71  42343  fourierdlem104  42376  fourierdlem112  42384  fouriersw  42397  etransclem46  42446  etransclem48  42448  nnfoctbdjlem  42618  sqrtnegnre  43388  fsummmodsnunz  43416  flsqrt5  43604  bits0ALTV  43691  mogoldbblem  43732  sgoldbeven3prm  43795  nnsum3primes4  43800  ushrisomgr  43853  smndex1n0mnd  43982  2zrngnmlid  44118  2zrngnmrid  44119  mpoexxg2  44284  lco0  44380  zlmodzxzldeplem3  44455  0dig1  44567  aacllem  44800
  Copyright terms: Public domain W3C validator