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

Theorem mpan2 690
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 686 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  mpanr12  704  mp3an23  1450  elvd  3486  eueq2  3687  sbcgf  3829  sbcralg  3841  csbconstgf  3884  sbcnestgw  4355  csbnestgw  4356  sbcnestg  4360  csbnestg  4361  csbnest1g  4364  mpteq1  5140  iinexg  5230  eusv2nf  5283  reusv2lem5  5290  nnullss  5341  xpss1  5561  xpiindi  5693  reldm0  5785  elrnmpt1s  5816  resdm  5884  eliniseg  5945  trinxp  5972  ssrnres  6022  cnveq0  6041  coi2  6103  relrelss  6111  cnviin  6124  ord0eln0  6232  funcnvres  6420  funimaex  6429  fnresin1  6461  fnresin2  6462  fresin  6537  ssimaex  6739  fvmpt  6759  fvmptnf  6781  fvimacnvALT  6818  dff3  6857  fsn  6888  fsn2  6889  funop  6902  fvrnressn  6914  fninfp  6927  fndifnfp  6929  fnnfpeq0  6931  fprb  6947  elabrex  6994  f1elima  7013  fliftel1  7056  f1owe  7099  sorpssuni  7452  sorpssint  7453  eldifpw  7484  ordeleqon  7497  ordsson  7498  ssnlim  7593  tposfun  7904  tpostpos2  7909  wfr3g  7949  wfrlem14  7964  wfrlem15  7965  tfrlem10  8019  tfrlem12  8021  tfr3  8031  seqomlem1  8082  seqomlem2  8083  seqomlem4  8085  ondif2  8123  oa0  8137  om0  8138  oa1suc  8152  om1  8164  oe1  8166  oe1m  8167  omass  8202  oeoalem  8218  oeoelem  8220  nnmsucr  8247  nnm1  8271  nnm2  8272  ecelqsg  8348  xpider  8364  mapdm0  8417  fvdiagfn  8451  ixpsnf1o  8498  xp1en  8599  sbthlem7  8630  domunsn  8664  xpmapenlem  8681  infensuc  8692  infi  8739  finresfin  8741  diffi  8747  findcard2d  8757  unblem1  8767  unblem2  8768  unblem3  8769  unblem4  8770  isfinite2  8773  infn0  8777  unfilem1  8779  unfilem2  8780  unfir  8783  fofinf1o  8796  cnvfi  8803  pwfilem  8815  mptfi  8820  finsschain  8828  marypha2  8900  inf0  9081  trcl  9167  r1rankidb  9230  snwf  9235  unwf  9236  uniwf  9245  rankval3b  9252  rankr1a  9262  rankxplim3  9307  scott0  9312  djueq1  9331  card1  9394  pm54.43  9427  infxpenc2  9446  dfac8clem  9456  alephsuc2  9504  alephle  9512  cardaleph  9513  dfac12lem2  9568  undjudom  9591  djudom1  9606  pwdju1  9614  ackbij1lem18  9657  cflem  9666  cflecard  9673  cfeq0  9676  cfslb  9686  cfsmolem  9690  cfcoflem  9692  cfidm  9695  isfin4p1  9735  fin23lem12  9751  fin23lem16  9755  fin23lem28  9760  fin23lem38  9769  fin23lem41  9772  fin1a2lem7  9826  fin1a2lem12  9831  fin1a2lem13  9832  hsmexlem8  9844  axcc2lem  9856  axcc3  9858  domtriomlem  9862  axdc3lem2  9871  axdc3lem4  9873  axdc4lem  9875  axcclem  9877  ac6num  9899  ttukeylem4  9932  ttukeylem7  9935  ttukey2g  9936  axdclem  9939  brdom3  9948  brdom5  9949  cardeq0  9972  unsnen  9973  konigthlem  9988  pwcfsdom  10003  canthp1lem1  10072  wunex2  10158  wuncval2  10167  eltsk2g  10171  ingru  10235  grutsk  10242  axgroth6  10248  mulidpi  10306  nlt1pi  10326  indpi  10327  pinq  10347  mulidnq  10383  1idpr  10449  prlem934  10453  0idsr  10517  1idsr  10518  00sr  10519  negexsr  10522  recexsrlem  10523  sqgt0sr  10526  ax1rid  10581  axcnre  10584  ne0gt0  10743  peano2cn  10810  peano2re  10811  00id  10813  mul02lem2  10815  mul01  10817  subid  10903  subid1  10904  negid  10931  negeq0  10938  peano2cnm  10950  peano2rem  10951  lt0neg1  11144  le0neg1  11146  relin01  11162  div2neg  11361  recgt0ii  11544  divgt0i2i  11553  ledivp1i  11563  ltdivp1i  11564  peano5nni  11637  peano2nn  11646  nnge1  11662  times2  11771  addltmul  11870  nn0p1nn  11933  peano2nn0  11934  nn0lele2xi  11949  frnnn0fsupp  11951  peano2z  12020  peano2zm  12022  suprzcl  12059  zeo  12065  uzwo  12308  uzwo2  12309  infssuzle  12328  infssuzcl  12329  zq  12351  rpnnen1lem1  12374  rpnnen1lem3  12375  rpnnen1lem5  12377  rphalfcl  12413  zgt1rpn0n1  12427  ltpnf  12512  nltmnf  12521  pnfge  12522  nltpnft  12554  xlemnf  12557  qsqueeze  12591  xlt0neg1  12609  xle0neg1  12611  xaddpnf1  12616  xaddmnf1  12618  xaddid1  12631  xsubge0  12651  xmul01  12657  xmulneg1  12659  xmulpnf1  12664  xmulid1  12669  supxrbnd  12718  supxrgtmnf  12719  supxrre1  12720  supxrre2  12721  elioopnf  12830  elicopnf  12832  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  fzprval  12972  fz0add1fz1  13111  fzofzp1  13138  fzostep1  13157  injresinj  13162  flge0nn0  13194  flge1nn  13195  btwnzge0  13202  modfrac  13256  om2uzsuci  13320  axdc4uzlem  13355  ser1const  13431  exp0  13438  exp1  13440  expn1  13444  nn0sqcl  13461  sqval  13486  sqeq0  13491  resqcl  13495  zsqcl  13499  expubnd  13546  binom21  13585  expnbnd  13598  nn0opthlem2  13634  bcnn  13677  bcn2  13684  bcn2p1  13690  bcnm1  13692  hasheq0  13729  hashsng  13735  hashen1  13736  hashunsnggt  13760  hashin  13777  hashdif  13779  hashgt23el  13790  hashxplem  13799  hashf1lem2  13819  hash2pr  13832  hash2prde  13833  pr2pwpr  13842  hash3tr  13853  iswrd  13868  wrdval  13869  hashwrdn  13899  ccatval2  13932  ccatrid  13941  eqs1  13966  s111  13969  ccatws1len  13974  repsw0  14139  repsw1  14145  cshw0  14156  wwlktovf  14320  relexpsucnnl  14391  reim0  14477  imval2  14510  cjne0  14522  abssq  14666  max0add  14670  abs2dif  14692  rddif  14700  absrdbnd  14701  rexuz3  14708  isershft  15020  isercolllem2  15022  isercoll  15024  fsum  15077  fsumadd  15096  fsumsplitsnun  15110  bcxmas  15190  infcvgaux2i  15213  fprod  15295  risefac0  15381  fallfac0  15382  risefac1  15387  fallfac1  15388  bpoly2  15411  bpoly3  15412  bpoly4  15413  fsumcube  15414  efi4p  15490  resin4p  15491  recos4p  15492  sinbnd  15533  cosbnd  15534  rpnnen2lem8  15574  rpnnen2lem12  15578  cnso  15600  dvdsmul2  15632  dvdslelem  15659  odd2np1lem  15689  mod2eq1n2dvds  15696  divalglem0  15742  divalglem1  15743  divalglem4  15745  divalglem5  15746  divalglem8  15749  flodddiv4  15762  bits0  15775  bitsp1o  15780  bitsf1  15793  sadadd2lem2  15797  gcd1  15874  gcdmultipleOLD  15898  lcm0val  15936  dvdslcm  15940  lcmeq0  15942  lcmgcd  15949  lcm1  15952  lcmfunsnlem2lem2  15981  lcmfunsnlem2  15982  prm2orodd  16033  phiprm  16112  pc0  16189  pcdvdstr  16210  vdwlem2  16316  vdwlem6  16320  vdwlem8  16322  hashbc0  16339  setsval  16513  fsets  16516  setsres  16525  ressinbas  16560  ressress  16562  elrestr  16702  pwssnf1o  16771  xpsfrnel  16835  xpscf  16838  ismred2  16874  submre  16876  mreacs  16929  oppchomfval  16984  brssc  17084  isssc  17090  yonedalem4c  17527  isprs  17540  oduleval  17741  oduclatb  17754  gsumval2a  17895  smndex1n0mnd  18077  mulg1  18235  mulgnegnn  18238  isghm  18358  ghmghmrn  18377  cntrnsg  18472  oppgplusfval  18476  pgrpsubgsymg  18537  psgneldm2i  18633  efgrelexlemb  18876  frgp0  18886  frgpmhm  18891  vrgpf  18894  cntrcmnd  18962  cntrabl  18963  cygctb  19012  dprd0  19153  dprd2da  19164  mgpplusg  19243  opprmulfval  19378  subrgint  19557  lsp0  19781  sralem  19949  rlmval2  19966  fczpsrbag  20147  ply1idvr1  20461  evls1rhmlem  20484  evl1fval1lem  20493  zringcyg  20638  mulgrhm2  20646  zlmsca  20668  chrnzr  20677  zrhpsgnelbas  20738  ocvz  20822  cssincl  20832  css0  20833  css1  20834  frlmip  20922  marrepeval  21172  decpmatid  21378  0opn  21512  topopn  21514  basdif0  21561  tgval  21563  isopn2  21640  0cld  21646  ntropn  21657  ntrval2  21659  ntrdif  21660  clsdif  21661  cmclsopn  21670  ntrtop  21678  ntr0  21689  mretopd  21700  neips  21721  neiptopnei  21740  maxlp  21755  isperf2  21760  rest0  21777  iocpnfordt  21823  icomnfordt  21824  mnfnei  21829  refref  22121  unisngl  22135  1stckgen  22162  ptbasfi  22189  pthaus  22246  fbssfi  22445  isfil2  22464  ssfg  22480  filconn  22491  fbasrn  22492  filufint  22528  imaelfm  22559  fmfnfmlem4  22565  fclsfnflim  22635  alexsubALTlem3  22657  alexsubALTlem4  22658  ustfilxp  22821  ustuqtop2  22851  ustuqtop4  22853  utopsnneiplem  22856  utopsnnei  22858  utop2nei  22859  cfiluweak  22904  neipcfilu  22905  xmetres  22974  metres  22975  mopnex  23129  prdsms  23141  metucn  23181  tngds  23257  tngngp3  23265  nmoge0  23330  cnfldnm  23387  tgioo  23404  xrtgioo  23414  xrsmopn  23420  negcncf  23530  phtpy01  23593  pco0  23622  tcphtopn  23833  tchnmfval  23835  caussi  23904  rrxip  23997  minveclem3b  24035  ovolfioo  24074  ovolficc  24075  ovolfsf  24078  ovolctb  24097  ovolctb2  24099  ovolfiniun  24108  ovoliun2  24113  ovolshftlem1  24116  ovolscalem1  24120  ovolicopnf  24131  iunmbl2  24164  uniioombllem2  24190  opnmblALT  24210  ismbf  24235  mbfinf  24272  0plef  24279  itg1climres  24321  itg2cnlem1  24368  iblitg  24375  ibl0  24393  itgcn  24451  cnlimc  24494  dvfre  24557  dvnfre  24558  dveflem  24585  dvef  24586  dvlipcn  24600  lhop2  24621  itgsubstlem  24654  deg1val  24700  ply1rem  24767  coefv0  24848  plyrecj  24879  vieta1lem2  24910  aannenlem1  24927  aaliou2b  24940  ulmval  24978  ulmpm  24981  ulmdvlem1  24998  mtest  25002  efcn  25041  sin2pim  25081  cos2pim  25082  sinmpi  25083  cosmpi  25084  sinppi  25085  cosppi  25086  efimpi  25087  sincosq1lem  25093  sincosq2sgn  25095  sincosq3sgn  25096  sincosq4sgn  25097  sinq12gt0  25103  sinq34lt0t  25105  sincosq1eq  25108  abssinper  25116  efif1o  25141  loglt1b  25228  relogcn  25232  ellogdm  25233  efopn  25252  cxp0  25264  cxp1  25265  cxpsqrt  25297  logsqrt  25298  logb1  25358  atandm3  25467  atanbnd  25515  atancn  25525  leibpi  25531  efrlim  25558  logdifbnd  25582  vmaprm  25705  ppip1le  25749  ppieq0  25764  prmorcht  25766  ppiublem1  25789  ppiub  25791  chpeq0  25795  chtub  25799  fsumvma  25800  pclogsum  25802  chpval2  25805  dchrresb  25846  dchrptlem1  25851  lgs0  25897  lgs2  25901  lgsdir2lem2  25913  lgsdir2lem4  25915  lgsdchrval  25941  lgsdchr  25942  lgseisenlem2  25963  2lgslem1c  25980  2lgsoddprmlem2  25996  addsq2nreurex  26031  dirith2  26115  selberg2lem  26137  qabvle  26212  qabvexp  26213  ostth  26226  istrkg2ld  26257  istrkg3ld  26258  ttgval  26672  cchhllem  26684  brbtwn  26696  colinearalglem4  26706  upgr0eop  26910  uspgrushgr  26971  usgruspgr  26974  usgr0eop  27039  0grsubgr  27071  uspgrloopvtx  27308  umgr2v2evtx  27314  usgr0edg0rusgr  27368  rgrusgrprc  27382  wlkvtxiedg  27417  pthdivtx  27521  usgr2pthlem  27555  wlkswwlksf1o  27668  wwlksext2clwwlk  27845  konigsbergssiedgw  28038  frgrncvvdeqlem7  28093  2clwwlk2  28136  ex-po  28223  pliguhgr  28272  nvnd  28474  ipval2lem3  28491  ipval2  28493  ipidsq  28496  dipcj  28500  dip0r  28503  nmlnogt0  28583  blocni  28591  ipasslem2  28618  ipasslem8  28623  ipasslem9  28624  ajval  28647  ubthlem1  28656  hvaddid2  28809  hvsub0  28862  hi02  28883  hlimi  28974  isch2  29009  chlimi  29020  chsupunss  29130  shsupunss  29132  chlejb1i  29262  h1dei  29336  h1de2ci  29342  spanunsni  29365  pjoml2i  29371  pjorthi  29455  mayete3i  29514  hosubid1  29584  nmopge0  29697  nmfnge0  29713  adj1  29719  adjeq  29721  lnop0  29752  lnopmi  29786  nmophmi  29817  cnlnadjlem5  29857  cnlnadjeui  29863  unierri  29890  leoprf2  29913  leopnmid  29924  nmopleid  29925  hstles  30017  hst0  30019  strlem3a  30038  dmdbr2  30089  mdsl1i  30107  mdsl2i  30108  mdsl2bi  30109  cvmdi  30110  mdslmd1lem1  30111  mdslmd1lem2  30112  mdslmd1i  30115  mdslmd2i  30116  csmdsymi  30120  mdexchi  30121  superpos  30140  atomli  30168  atordi  30170  chirredlem1  30176  chirredlem2  30177  atcvat4i  30183  atabsi  30187  mdsymlem1  30189  mdsymlem5  30193  mdsymlem6  30194  sumdmdii  30201  dmdbr5ati  30208  dmdbr6ati  30209  mddmdin0i  30217  cdj3lem2  30221  unidifsnel  30306  unidifsnne  30307  xppreima  30405  abfmpunirn  30408  abfmpel  30411  aciunf1lem  30418  fgreu  30428  imafi2  30458  padct  30466  fpwrelmapffslem  30479  fpwrelmap  30480  xrge0infss  30495  xrdifh  30514  pfx1s2  30626  clatp0cl  30669  clatp1cl  30670  cntrcrng  30729  cycpmco2lem4  30803  rmfsupp2  30899  resvval  30933  rearchi  30948  qusxpid  30961  locfinreflem  31164  locfinref  31165  ordtconnlem1  31224  rge0scvg  31249  lmxrge0  31252  qqh0  31282  qqh1  31283  rrh0  31313  zrhre  31317  esumcst  31379  esumfzf  31385  esumfsupre  31387  hasheuni  31401  sgon  31440  dmvlsiga  31445  sigainb  31452  measval  31514  ismeas  31515  sxbrsigalem0  31586  omssubadd  31615  carsggect  31633  eulerpartlemmf  31690  eulerpartlemgs2  31695  eulerpartlemn  31696  rrvsum  31769  ballotlem2  31803  ballotlemfcc  31808  ballotlem4  31813  signsplypnf  31877  signsply0  31878  signsw0glem  31880  signswrid  31885  signlem0  31914  signshf  31915  bnj535  32219  bnj580  32242  bnj907  32296  bnj1253  32346  funen1cnv  32414  loop1cycl  32441  ptpconn  32537  cvmsss2  32578  cvmlift2lem12  32618  cvmlift2lem13  32619  cvmliftphtlem  32621  cvmliftpht  32622  fmlafvel  32689  mppsthm  32883  bcneg1  33025  fv1stcnv  33077  fv2ndcnv  33078  trpred0  33132  wlimeq1  33164  frr3g  33178  fpr3g  33179  noextendseq  33231  noetalem3  33276  scutun12  33328  imagesset  33471  altopeq1  33481  brcolinear2  33576  cldbnd  33731  ivthALT  33740  refssfne  33763  ontgval  33836  onint1  33854  axc11n11r  34074  bj-bm1.3ii  34425  bj-restsn0  34444  bj-restsn10  34445  bj-restsnid  34446  bj-rest10  34447  bj-rest0  34452  bj-inftyexpiinv  34568  bj-inftyexpidisj  34570  taupilem1  34680  irrdiff  34685  f1omptsnlem  34698  mptsnunlem  34700  topdifinffinlem  34709  inunissunidif  34737  rdgssun  34740  exrecfnlem  34741  exrecfnpw  34743  finixpnum  34987  tan2h  34994  matunitlindflem2  34999  ptrest  35001  poimirlem22  35024  poimirlem25  35027  mblfinlem1  35039  mblfinlem2  35040  mblfinlem3  35041  mblfinlem4  35042  ismblfin  35043  itg2addnclem  35053  itg2addnclem2  35054  itg2addnclem3  35055  itg2addnc  35056  itg2gt0cn  35057  ftc1anclem5  35079  ftc1anclem8  35082  dvasin  35086  dvacos  35087  sdclem2  35125  totbndbnd  35172  heibor1lem  35192  heiborlem7  35200  bfplem1  35205  prnc  35450  ecexALTV  35693  brxrn  35731  riotasv  36200  glbconN  36618  atpointN  36984  polsubN  37148  pol0N  37150  pol1N  37151  2polvalN  37155  2polssN  37156  3polN  37157  pcl0N  37163  2pmaplubN  37167  pnonsingN  37174  polsubclN  37193  cdlemefs32sn1aw  37655  cdleme43fsv1snlem  37661  cdleme41sn3a  37674  cdleme32a  37682  cdleme40m  37708  cdleme40n  37709  cdleme42b  37719  istendo  38001  cdlemk40  38158  cdlemkid  38177  dihvalcqpre  38476  facp2  39293  fac2xp3  39322  2xp3dxp2ge1d  39324  factwoffsmonot  39325  fnsnbt  39348  frlmsnic  39387  sn-inelr  39510  0prjspn  39530  3cubes  39547  mapfzcons1cl  39575  eldioph3b  39622  eldiophss  39631  0dioph  39635  vdioph  39636  eldioph4b  39668  eldioph4i  39669  rencldnfilem  39677  rmxy1  39779  rmxy0  39780  rmxm1  39791  rmym1  39792  monotoddzzfi  39799  aomclem6  39919  pwslnmlem0  39951  isnumbasabl  39966  areaquad  40082  reabsifneg  40248  reabsifnneg  40251  relexp2  40294  eltrclrec  40297  elrtrclrec  40298  brtrclrec  40313  brrtrclrec  40314  relexpxpmin  40334  dftrcl3  40337  dfrtrcl3  40350  heeq1  40395  seff  40933  lhe4.4ex1a  40953  eelT0  41401  snssl  41456  sineq0ALT  41563  elabrexg  41595  elrnmpt1sf  41741  founiiun0  41742  supxrgere  41891  supxrgelem  41895  fmuldfeqlem1  42150  fmuldfeq  42151  climneg  42178  sumnnodd  42198  liminfltlem  42372  xlimpnfxnegmnf2  42426  addccncf2  42444  dvsinax  42481  stoweidlem18  42586  stoweidlem19  42587  stoweidlem22  42590  stoweidlem34  42602  stoweidlem40  42608  stoweidlem41  42609  stoweidlem55  42623  stoweidlem59  42627  dirker2re  42660  dirkerdenne0  42661  fourierdlem48  42722  fourierdlem49  42723  fourierdlem70  42744  fourierdlem71  42745  fourierdlem104  42778  fourierdlem112  42786  fouriersw  42799  etransclem46  42848  etransclem48  42850  nnfoctbdjlem  43020  sqrtnegnre  43790  fsummmodsnunz  43818  flsqrt5  44037  bits0ALTV  44123  mogoldbblem  44164  sgoldbeven3prm  44227  nnsum3primes4  44232  ushrisomgr  44285  2zrngnmlid  44499  2zrngnmrid  44500  mpoexxg2  44665  lco0  44762  zlmodzxzldeplem3  44837  0dig1  44949  naryfvalel  44970  ackvalsuc0val  45027  aacllem  45255
  Copyright terms: Public domain W3C validator