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  3498  eueq2  3698  sbcgf  3842  sbcralg  3854  csbconstgf  3898  sbcnestgw  4369  csbnestgw  4370  sbcnestg  4374  csbnestg  4375  csbnest1g  4378  mpteq1  5145  iinexg  5235  eusv2nf  5286  reusv2lem5  5293  nnullss  5345  xpss1  5567  xpiindi  5699  reldm0  5791  elrnmpt1s  5822  resdm  5890  eliniseg  5951  trinxp  5978  ssrnres  6028  cnveq0  6047  coi2  6109  relrelss  6117  cnviin  6130  ord0eln0  6238  funcnvres  6425  funimaex  6434  fnresin1  6465  fnresin2  6466  fresin  6540  ssimaex  6741  fvmpt  6761  fvmptnf  6782  fvimacnvALT  6819  dff3  6858  fsn  6889  fsn2  6890  funop  6903  fvrnressn  6915  fninfp  6928  fndifnfp  6930  fnnfpeq0  6932  fprb  6948  elabrex  6993  f1elima  7012  fliftel1  7052  f1owe  7095  sorpssuni  7447  sorpssint  7448  eldifpw  7479  ordeleqon  7492  ordsson  7493  ssnlim  7588  tposfun  7897  tpostpos2  7902  wfr3g  7942  wfrlem14  7957  wfrlem15  7958  tfrlem10  8012  tfrlem12  8014  tfr3  8024  seqomlem1  8075  seqomlem2  8076  seqomlem4  8078  ondif2  8116  oa0  8130  om0  8131  oa1suc  8145  om1  8157  oe1  8159  oe1m  8160  omass  8195  oeoalem  8211  oeoelem  8213  nnmsucr  8240  nnm1  8264  nnm2  8265  ecelqsg  8341  xpider  8357  mapdm0  8410  fvdiagfn  8443  ixpsnf1o  8490  xp1en  8591  sbthlem7  8621  domunsn  8655  xpmapenlem  8672  infensuc  8683  infi  8730  finresfin  8732  diffi  8738  findcard2d  8748  unblem1  8758  unblem2  8759  unblem3  8760  unblem4  8761  isfinite2  8764  infn0  8768  unfilem1  8770  unfilem2  8771  unfir  8774  fofinf1o  8787  cnvfi  8794  pwfilem  8806  mptfi  8811  finsschain  8819  marypha2  8891  inf0  9072  trcl  9158  r1rankidb  9221  snwf  9226  unwf  9227  uniwf  9236  rankval3b  9243  rankr1a  9253  rankxplim3  9298  scott0  9303  djueq1  9322  card1  9385  pm54.43  9417  infxpenc2  9436  dfac8clem  9446  alephsuc2  9494  alephle  9502  cardaleph  9503  dfac12lem2  9558  undjudom  9581  djudom1  9596  pwdju1  9604  ackbij1lem18  9647  cflem  9656  cflecard  9663  cfeq0  9666  cfslb  9676  cfsmolem  9680  cfcoflem  9682  cfidm  9685  isfin4p1  9725  fin23lem12  9741  fin23lem16  9745  fin23lem28  9750  fin23lem38  9759  fin23lem41  9762  fin1a2lem7  9816  fin1a2lem12  9821  fin1a2lem13  9822  hsmexlem8  9834  axcc2lem  9846  axcc3  9848  domtriomlem  9852  axdc3lem2  9861  axdc3lem4  9863  axdc4lem  9865  axcclem  9867  ac6num  9889  ttukeylem4  9922  ttukeylem7  9925  ttukey2g  9926  axdclem  9929  brdom3  9938  brdom5  9939  cardeq0  9962  unsnen  9963  konigthlem  9978  pwcfsdom  9993  canthp1lem1  10062  wunex2  10148  wuncval2  10157  eltsk2g  10161  ingru  10225  grutsk  10232  axgroth6  10238  mulidpi  10296  nlt1pi  10316  indpi  10317  pinq  10337  mulidnq  10373  1idpr  10439  prlem934  10443  0idsr  10507  1idsr  10508  00sr  10509  negexsr  10512  recexsrlem  10513  sqgt0sr  10516  ax1rid  10571  axcnre  10574  ne0gt0  10733  peano2cn  10800  peano2re  10801  00id  10803  mul02lem2  10805  mul01  10807  subid  10893  subid1  10894  negid  10921  negeq0  10928  peano2cnm  10940  peano2rem  10941  lt0neg1  11134  le0neg1  11136  relin01  11152  div2neg  11351  recgt0ii  11534  divgt0i2i  11543  ledivp1i  11553  ltdivp1i  11554  peano5nni  11629  peano2nn  11638  nnge1  11653  times2  11762  addltmul  11861  nn0p1nn  11924  peano2nn0  11925  nn0lele2xi  11940  frnnn0fsupp  11942  peano2z  12011  peano2zm  12013  suprzcl  12050  zeo  12056  uzwo  12299  uzwo2  12300  infssuzle  12319  infssuzcl  12320  zq  12342  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  rphalfcl  12404  zgt1rpn0n1  12418  ltpnf  12503  nltmnf  12512  pnfge  12513  nltpnft  12545  xlemnf  12548  qsqueeze  12582  xlt0neg1  12600  xle0neg1  12602  xaddpnf1  12607  xaddmnf1  12609  xaddid1  12622  xsubge0  12642  xmul01  12648  xmulneg1  12650  xmulpnf1  12655  xmulid1  12660  supxrbnd  12709  supxrgtmnf  12710  supxrre1  12711  supxrre2  12712  elioopnf  12819  elicopnf  12821  iccshftri  12861  iccshftli  12863  iccdili  12865  icccntri  12867  fzprval  12956  fz0add1fz1  13095  fzofzp1  13122  fzostep1  13141  injresinj  13146  flge0nn0  13178  flge1nn  13179  btwnzge0  13186  modfrac  13240  om2uzsuci  13304  axdc4uzlem  13339  ser1const  13414  exp0  13421  exp1  13423  expn1  13427  nn0sqcl  13444  sqval  13469  sqeq0  13474  resqcl  13478  zsqcl  13482  expubnd  13529  binom21  13568  expnbnd  13581  nn0opthlem2  13617  bcnn  13660  bcn2  13667  bcn2p1  13673  bcnm1  13675  hasheq0  13712  hashsng  13718  hashen1  13719  hashunsnggt  13743  hashin  13760  hashdif  13762  hashgt23el  13773  hashxplem  13782  hashf1lem2  13802  hash2pr  13815  hash2prde  13816  pr2pwpr  13825  hash3tr  13836  iswrd  13851  wrdval  13852  wrdvOLD  13866  hashwrdn  13886  ccatval2  13920  ccatrid  13929  eqs1  13954  s111  13957  ccatws1len  13962  repsw0  14127  repsw1  14133  cshw0  14144  wwlktovf  14308  relexpsucnnl  14379  reim0  14465  imval2  14498  cjne0  14510  abssq  14654  max0add  14658  abs2dif  14680  rddif  14688  absrdbnd  14689  rexuz3  14696  isershft  15008  isercolllem2  15010  isercoll  15012  fsum  15065  fsumadd  15084  fsumsplitsnun  15098  bcxmas  15178  infcvgaux2i  15201  fprod  15283  risefac0  15369  fallfac0  15370  risefac1  15375  fallfac1  15376  bpoly2  15399  bpoly3  15400  bpoly4  15401  fsumcube  15402  efi4p  15478  resin4p  15479  recos4p  15480  sinbnd  15521  cosbnd  15522  rpnnen2lem8  15562  rpnnen2lem12  15566  cnso  15588  dvdsmul2  15620  dvdslelem  15647  odd2np1lem  15677  mod2eq1n2dvds  15684  divalglem0  15732  divalglem1  15733  divalglem4  15735  divalglem5  15736  divalglem8  15739  flodddiv4  15752  bits0  15765  bitsp1o  15770  bitsf1  15783  sadadd2lem2  15787  gcd1  15864  gcdmultipleOLD  15888  lcm0val  15926  dvdslcm  15930  lcmeq0  15932  lcmgcd  15939  lcm1  15942  lcmfunsnlem2lem2  15971  lcmfunsnlem2  15972  prm2orodd  16023  phiprm  16102  pc0  16179  pcdvdstr  16200  vdwlem2  16306  vdwlem6  16310  vdwlem8  16312  hashbc0  16329  setsval  16501  fsets  16504  setsres  16513  ressinbas  16548  ressress  16550  elrestr  16690  pwssnf1o  16759  xpsfrnel  16823  xpscf  16826  ismred2  16862  submre  16864  mreacs  16917  oppchomfval  16972  brssc  17072  isssc  17078  yonedalem4c  17515  isprs  17528  oduleval  17729  oduclatb  17742  gsumval2a  17883  mulg1  18173  mulgnegnn  18176  isghm  18296  ghmghmrn  18315  cntrnsg  18410  oppgplusfval  18414  psgneldm2i  18562  efgrelexlemb  18805  frgp0  18815  frgpmhm  18820  vrgpf  18823  cntrcmnd  18891  cntrabl  18892  cygctb  18941  dprd0  19082  dprd2da  19093  mgpplusg  19172  opprmulfval  19304  subrgint  19486  lsp0  19710  sralem  19878  rlmval2  19895  fczpsrbag  20075  ply1idvr1  20389  evls1rhmlem  20412  evl1fval1lem  20421  zringcyg  20566  mulgrhm2  20574  zlmsca  20596  chrnzr  20605  zrhpsgnelbas  20666  ocvz  20750  cssincl  20760  css0  20761  css1  20762  frlmip  20850  marrepeval  21100  decpmatid  21306  0opn  21440  topopn  21442  basdif0  21489  tgval  21491  isopn2  21568  0cld  21574  ntropn  21585  ntrval2  21587  ntrdif  21588  clsdif  21589  cmclsopn  21598  ntrtop  21606  ntr0  21617  mretopd  21628  neips  21649  neiptopnei  21668  maxlp  21683  isperf2  21688  rest0  21705  iocpnfordt  21751  icomnfordt  21752  mnfnei  21757  refref  22049  unisngl  22063  1stckgen  22090  ptbasfi  22117  pthaus  22174  fbssfi  22373  isfil2  22392  ssfg  22408  filconn  22419  fbasrn  22420  filufint  22456  imaelfm  22487  fmfnfmlem4  22493  fclsfnflim  22563  alexsubALTlem3  22585  alexsubALTlem4  22586  ustfilxp  22748  ustuqtop2  22778  ustuqtop4  22780  utopsnneiplem  22783  utopsnnei  22785  utop2nei  22786  cfiluweak  22831  neipcfilu  22832  xmetres  22901  metres  22902  mopnex  23056  prdsms  23068  metucn  23108  tngds  23184  tngngp3  23192  nmoge0  23257  cnfldnm  23314  tgioo  23331  xrtgioo  23341  xrsmopn  23347  negcncf  23453  phtpy01  23516  pco0  23545  tcphtopn  23756  tchnmfval  23758  caussi  23827  rrxip  23920  minveclem3b  23958  ovolfioo  23995  ovolficc  23996  ovolfsf  23999  ovolctb  24018  ovolctb2  24020  ovolfiniun  24029  ovoliun2  24034  ovolshftlem1  24037  ovolscalem1  24041  ovolicopnf  24052  iunmbl2  24085  uniioombllem2  24111  opnmblALT  24131  ismbf  24156  mbfinf  24193  0plef  24200  itg1climres  24242  itg2cnlem1  24289  iblitg  24296  ibl0  24314  itgcn  24370  cnlimc  24413  dvfre  24475  dvnfre  24476  dveflem  24503  dvef  24504  dvlipcn  24518  lhop2  24539  itgsubstlem  24572  deg1val  24617  ply1rem  24684  coefv0  24765  plyrecj  24796  vieta1lem2  24827  aannenlem1  24844  aaliou2b  24857  ulmval  24895  ulmpm  24898  ulmdvlem1  24915  mtest  24919  efcn  24958  sin2pim  24998  cos2pim  24999  sinmpi  25000  cosmpi  25001  sinppi  25002  cosppi  25003  efimpi  25004  sincosq1lem  25010  sincosq2sgn  25012  sincosq3sgn  25013  sincosq4sgn  25014  sinq12gt0  25020  sinq34lt0t  25022  sincosq1eq  25025  abssinper  25033  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  25447  efrlim  25474  logdifbnd  25498  vmaprm  25621  ppip1le  25665  ppieq0  25680  prmorcht  25682  ppiublem1  25705  ppiub  25707  chpeq0  25711  chtub  25715  fsumvma  25716  pclogsum  25718  chpval2  25721  dchrresb  25762  dchrptlem1  25767  lgs0  25813  lgs2  25817  lgsdir2lem2  25829  lgsdir2lem4  25831  lgsdchrval  25857  lgsdchr  25858  lgseisenlem2  25879  2lgslem1c  25896  2lgsoddprmlem2  25912  addsq2nreurex  25947  dirith2  26031  selberg2lem  26053  qabvle  26128  qabvexp  26129  ostth  26142  istrkg2ld  26173  istrkg3ld  26174  ttgval  26588  cchhllem  26600  brbtwn  26612  colinearalglem4  26622  upgr0eop  26826  uspgrushgr  26887  usgruspgr  26890  usgr0eop  26955  0grsubgr  26987  uspgrloopvtx  27224  umgr2v2evtx  27230  usgr0edg0rusgr  27284  rgrusgrprc  27298  wlkvtxiedg  27333  pthdivtx  27437  usgr2pthlem  27471  wlkswwlksf1o  27584  wwlksext2clwwlk  27763  konigsbergssiedgw  27956  frgrncvvdeqlem7  28011  2clwwlk2  28054  ex-po  28141  pliguhgr  28190  nvnd  28392  ipval2lem3  28409  ipval2  28411  ipidsq  28414  dipcj  28418  dip0r  28421  nmlnogt0  28501  blocni  28509  ipasslem2  28536  ipasslem8  28541  ipasslem9  28542  ajval  28565  ubthlem1  28574  hvaddid2  28727  hvsub0  28780  hi02  28801  hlimi  28892  isch2  28927  chlimi  28938  chsupunss  29048  shsupunss  29050  chlejb1i  29180  h1dei  29254  h1de2ci  29260  spanunsni  29283  pjoml2i  29289  pjorthi  29373  mayete3i  29432  hosubid1  29502  nmopge0  29615  nmfnge0  29631  adj1  29637  adjeq  29639  lnop0  29670  lnopmi  29704  nmophmi  29735  cnlnadjlem5  29775  cnlnadjeui  29781  unierri  29808  leoprf2  29831  leopnmid  29842  nmopleid  29843  hstles  29935  hst0  29937  strlem3a  29956  dmdbr2  30007  mdsl1i  30025  mdsl2i  30026  mdsl2bi  30027  cvmdi  30028  mdslmd1lem1  30029  mdslmd1lem2  30030  mdslmd1i  30033  mdslmd2i  30034  csmdsymi  30038  mdexchi  30039  superpos  30058  atomli  30086  atordi  30088  chirredlem1  30094  chirredlem2  30095  atcvat4i  30101  atabsi  30105  mdsymlem1  30107  mdsymlem5  30111  mdsymlem6  30112  sumdmdii  30119  dmdbr5ati  30126  dmdbr6ati  30127  mddmdin0i  30135  cdj3lem2  30139  unidifsnel  30222  unidifsnne  30223  xppreima  30322  abfmpunirn  30325  abfmpel  30328  aciunf1lem  30335  fgreu  30345  imafi2  30373  padct  30381  fpwrelmapffslem  30394  fpwrelmap  30395  xrge0infss  30410  xrdifh  30429  pfx1s2  30542  clatp0cl  30585  clatp1cl  30586  cntrcrng  30624  cycpmco2lem4  30698  rmfsupp2  30793  resvval  30827  rearchi  30842  qusxpid  30855  locfinreflem  31003  locfinref  31004  ordtconnlem1  31066  rge0scvg  31091  lmxrge0  31094  qqh0  31124  qqh1  31125  rrh0  31155  zrhre  31159  esumcst  31221  esumfzf  31227  esumfsupre  31229  hasheuni  31243  sgon  31282  dmvlsiga  31287  sigainb  31294  measval  31356  ismeas  31357  sxbrsigalem0  31428  omssubadd  31457  carsggect  31475  eulerpartlemmf  31532  eulerpartlemgs2  31537  eulerpartlemn  31538  rrvsum  31611  ballotlem2  31645  ballotlemfcc  31650  ballotlem4  31655  signsplypnf  31719  signsply0  31720  signsw0glem  31722  signswrid  31727  signlem0  31756  signshf  31757  bnj535  32061  bnj580  32084  bnj907  32136  bnj1253  32186  funen1cnv  32254  loop1cycl  32281  ptpconn  32377  cvmsss2  32418  cvmlift2lem12  32458  cvmlift2lem13  32459  cvmliftphtlem  32461  cvmliftpht  32462  fmlafvel  32529  mppsthm  32723  bcneg1  32865  fv1stcnv  32917  fv2ndcnv  32918  trpred0  32972  wlimeq1  33004  frr3g  33018  fpr3g  33019  noextendseq  33071  noetalem3  33116  scutun12  33168  imagesset  33311  altopeq1  33321  brcolinear2  33416  cldbnd  33571  ivthALT  33580  refssfne  33603  ontgval  33676  onint1  33694  axc11n11r  33914  bj-bm1.3ii  34251  bj-restsn0  34270  bj-restsn10  34271  bj-restsnid  34272  bj-rest10  34273  bj-rest0  34278  bj-inftyexpiinv  34382  bj-inftyexpidisj  34384  taupilem1  34484  f1omptsnlem  34499  mptsnunlem  34501  topdifinffinlem  34510  inunissunidif  34538  rdgssun  34541  exrecfnlem  34542  exrecfnpw  34544  finixpnum  34758  tan2h  34765  matunitlindflem2  34770  ptrest  34772  poimirlem22  34795  poimirlem25  34798  mblfinlem1  34810  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  ismblfin  34814  itg2addnclem  34824  itg2addnclem2  34825  itg2addnclem3  34826  itg2addnc  34827  itg2gt0cn  34828  ftc1anclem5  34852  ftc1anclem8  34855  dvasin  34859  dvacos  34860  sdclem2  34898  totbndbnd  34948  heibor1lem  34968  heiborlem7  34976  bfplem1  34981  prnc  35226  ecexALTV  35469  brxrn  35506  riotasv  35975  glbconN  36393  atpointN  36759  polsubN  36923  pol0N  36925  pol1N  36926  2polvalN  36930  2polssN  36931  3polN  36932  pcl0N  36938  2pmaplubN  36942  pnonsingN  36949  polsubclN  36968  cdlemefs32sn1aw  37430  cdleme43fsv1snlem  37436  cdleme41sn3a  37449  cdleme32a  37457  cdleme40m  37483  cdleme40n  37484  cdleme42b  37494  istendo  37776  cdlemk40  37933  cdlemkid  37952  dihvalcqpre  38251  fnsnbt  38998  frlmsnic  39027  0prjspn  39148  3cubes  39165  mapfzcons1cl  39193  eldioph3b  39240  eldiophss  39249  0dioph  39253  vdioph  39254  eldioph4b  39286  eldioph4i  39287  rencldnfilem  39295  rmxy1  39397  rmxy0  39398  rmxm1  39409  rmym1  39410  monotoddzzfi  39417  aomclem6  39537  pwslnmlem0  39569  isnumbasabl  39584  areaquad  39701  relexp2  39900  eltrclrec  39903  elrtrclrec  39904  brtrclrec  39919  brrtrclrec  39920  relexpxpmin  39940  dftrcl3  39943  dfrtrcl3  39956  heeq1  40001  seff  40518  lhe4.4ex1a  40538  eelT0  40986  snssl  41041  sineq0ALT  41148  elabrexg  41180  elrnmpt1sf  41326  founiiun0  41327  supxrgere  41477  supxrgelem  41481  fmuldfeqlem1  41739  fmuldfeq  41740  climneg  41767  sumnnodd  41787  liminfltlem  41961  xlimpnfxnegmnf2  42015  addccncf2  42035  dvsinax  42073  stoweidlem18  42180  stoweidlem19  42181  stoweidlem22  42184  stoweidlem34  42196  stoweidlem40  42202  stoweidlem41  42203  stoweidlem55  42217  stoweidlem59  42221  dirker2re  42254  dirkerdenne0  42255  fourierdlem48  42316  fourierdlem49  42317  fourierdlem70  42338  fourierdlem71  42339  fourierdlem104  42372  fourierdlem112  42380  fouriersw  42393  etransclem46  42442  etransclem48  42444  nnfoctbdjlem  42614  sqrtnegnre  43384  fsummmodsnunz  43412  flsqrt5  43634  bits0ALTV  43721  mogoldbblem  43762  sgoldbeven3prm  43825  nnsum3primes4  43830  ushrisomgr  43883  smndex1n0mnd  44012  2zrngnmlid  44148  2zrngnmrid  44149  mpoexxg2  44314  lco0  44410  zlmodzxzldeplem3  44485  0dig1  44597  aacllem  44830
  Copyright terms: Public domain W3C validator