Theorem mpan2 674

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

Step	Hyp	Ref	Expression
1		mpan2.1	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		mpan2.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	2, 3	mpdan 670	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  mpanr12  688  mp3an23  1570  elvd  3403  eueq2  3585  sbcgf  3704  sbcralg  3715  csbconstgf  3747  sbcnestg  4201  csbnestg  4202  csbnest1g  4205  mpteq1  4938  iinexg  5023  eusv2nf  5071  reusv2lem5  5078  nnullss  5127  xpss1  5336  xpiindi  5466  reldm0  5551  elrnmpt1s  5581  residOLD  5649  resdm  5653  eliniseg  5711  trinxp  5739  ssrnres  5790  cnveq0  5809  coi2  5873  relrelss  5880  cnviin  5893  ord0eln0  5998  funcnvres  6181  funimaex  6190  fnresin1  6219  fnresin2  6220  fresin  6291  ssimaex  6487  fvmpt  6506  fvmptnf  6526  fvimacnvALT  6561  dff3  6597  fsn  6628  fsn2  6629  funop  6641  fvrnressn  6655  fninfp  6668  fndifnfp  6670  fnnfpeq0  6672  elabrex  6728  f1elima  6747  fliftel1  6787  f1owe  6830  sorpssuni  7179  sorpssint  7180  eldifpw  7209  ordeleqon  7221  ordsson  7222  ssnlim  7316  tposfun  7606  tpostpos2  7611  wfr3g  7651  wfrlem14  7667  wfrlem15  7668  tfrlem10  7722  tfrlem12  7724  tfr3  7734  seqomlem1  7784  seqomlem2  7785  seqomlem4  7787  ondif2  7822  oa0  7836  om0  7837  oa1suc  7851  om1  7862  oe1  7864  oe1m  7865  omass  7900  oeoalem  7916  oeoelem  7918  nnmsucr  7945  nnm1  7968  nnm2  7969  ecelqsg  8040  xpider  8056  mapdm0  8110  map0eOLD  8134  fvdiagfn  8142  ixpsnf1o  8188  xp1en  8288  sbthlem7  8318  domunsn  8352  xpmapenlem  8369  infensuc  8380  infi  8426  finresfin  8428  diffi  8434  findcard2d  8444  unblem1  8454  unblem2  8455  unblem3  8456  unblem4  8457  isfinite2  8460  infn0  8464  unfilem1  8466  unfilem2  8467  unfir  8470  fofinf1o  8483  cnvfi  8490  pwfilem  8502  mptfi  8507  finsschain  8515  marypha2  8587  inf0  8768  trcl  8854  r1rankidb  8917  snwf  8922  unwf  8923  uniwf  8932  rankval3b  8939  rankr1a  8949  rankxplim3  8994  scott0  8999  djueq1  9018  card1  9080  pm54.43  9112  infxpenc2  9131  dfac8clem  9141  alephsuc2  9189  alephle  9197  cardaleph  9198  dfac12lem2  9254  cdaval  9280  uncdadom  9281  cdaun  9282  cdacomen  9291  cdaassen  9292  cdadom1  9296  cdainf  9302  pwcda1  9304  ackbij1lem18  9347  cflem  9356  cflecard  9363  cfeq0  9366  cfslb  9376  cfsmolem  9380  cfcoflem  9382  cfidm  9385  isfin4-3  9425  fin23lem12  9441  fin23lem16  9445  fin23lem28  9450  fin23lem38  9459  fin23lem41  9462  fin1a2lem7  9516  fin1a2lem12  9521  fin1a2lem13  9522  hsmexlem8  9534  axcc2lem  9546  axcc3  9548  domtriomlem  9552  axdc3lem2  9561  axdc3lem4  9563  axdc4lem  9565  axcclem  9567  ac6num  9589  ttukeylem4  9622  ttukeylem7  9625  ttukey2g  9626  axdclem  9629  brdom3  9638  brdom5  9639  cardeq0  9662  unsnen  9663  konigthlem  9678  pwcfsdom  9693  canthp1lem1  9762  wunex2  9848  wuncval2  9857  eltsk2g  9861  ingru  9925  grutsk  9932  axgroth6  9938  mulidpi  9996  nlt1pi  10016  indpi  10017  pinq  10037  mulidnq  10073  1idpr  10139  prlem934  10143  0idsr  10206  1idsr  10207  00sr  10208  negexsr  10211  recexsrlem  10212  sqgt0sr  10215  ax1rid  10270  axcnre  10273  ne0gt0  10430  peano2cn  10496  peano2re  10497  00id  10499  mul02lem2  10501  mul01  10503  subid  10588  subid1  10589  negid  10616  negeq0  10623  peano2cnm  10635  peano2rem  10636  lt0neg1  10822  le0neg1  10824  relin01  10840  div2neg  11036  recgt0ii  11217  divgt0i2i  11227  ledivp1i  11237  ltdivp1i  11238  peano5nni  11311  peano2nn  11320  nnge1  11335  times2  11432  addltmul  11538  nn0p1nn  11601  peano2nn0  11602  nn0lele2xi  11617  frnnn0fsupp  11619  peano2z  11687  peano2zm  11689  suprzcl  11726  zeo  11732  uzwo  11973  uzwo2  11974  infssuzle  11993  infssuzcl  11994  rpnnen1lem1  12037  rpnnen1lem3  12038  rpnnen1lem5  12040  rphalfcl  12075  zgt1rpn0n1  12088  ltpnf  12173  nltmnf  12182  pnfge  12183  nltpnft  12216  xlemnf  12219  qsqueeze  12253  xlt0neg1  12271  xle0neg1  12273  xaddpnf1  12278  xaddmnf1  12280  xaddid1  12293  xsubge0  12312  xmul01  12318  xmulneg1  12320  xmulpnf1  12325  xmulid1  12330  supxrbnd  12379  supxrgtmnf  12380  supxrre1  12381  supxrre2  12382  elioopnf  12489  elicopnf  12491  xrge0neqmnfOLD  12499  iccshftri  12533  iccshftli  12535  iccdili  12537  icccntri  12539  fzprval  12627  fz0add1fz1  12765  fzofzp1  12792  fzostep1  12811  injresinj  12816  flge0nn0  12848  flge1nn  12849  btwnzge0  12856  modfrac  12910  om2uzsuci  12974  axdc4uzlem  13009  ser1const  13083  exp0  13090  exp1  13092  expn1  13096  nn0sqcl  13113  expubnd  13147  sqval  13148  sqeq0  13153  resqcl  13157  zsqcl  13160  binom21  13206  expnbnd  13219  nn0opthlem2  13279  bcnn  13322  bcn2  13329  bcn2p1  13335  bcnm1  13337  hasheq0  13375  hashsng  13380  hashen1  13381  hashin  13419  hashdif  13421  hashxplem  13440  hashf1lem2  13460  hash2pr  13471  hash2prde  13472  pr2pwpr  13481  hash3tr  13492  iswrd  13521  wrdval  13522  wrdv  13534  ccatval2  13578  ccatrid  13587  s111  13613  swrd0len0  13663  repsw0  13751  repsw1  13757  cshw0  13767  wwlktovf  13927  relexpsucnnl  13998  reim0  14084  imval2  14117  cjne0  14129  abssq  14272  max0add  14276  abs2dif  14298  rddif  14306  absrdbnd  14307  rexuz3  14314  isershft  14620  isercolllem2  14622  isercoll  14624  fsum  14677  fsumadd  14696  fsumsplitsnun  14710  fsumsplitsnunOLD  14712  bcxmas  14792  infcvgaux2i  14815  fprod  14895  risefac0  14981  fallfac0  14982  risefac1  14987  fallfac1  14988  bpoly2  15011  bpoly3  15012  bpoly4  15013  fsumcube  15014  efi4p  15090  resin4p  15091  recos4p  15092  sinbnd  15133  cosbnd  15134  znnenlemOLD  15163  rpnnen2lem8  15173  rpnnen2lem12  15177  cnso  15199  dvdsmul2  15230  dvdslelem  15257  odd2np1lem  15287  mod2eq1n2dvds  15294  divalglem0  15339  divalglem1  15340  divalglem4  15342  divalglem5  15343  divalglem8  15346  flodddiv4  15359  bits0  15372  bitsp1o  15377  bitsf1  15390  sadadd2lem2  15394  gcd1  15471  gcdmultiple  15491  lcm0val  15529  dvdslcm  15533  lcmeq0  15535  lcmgcd  15542  lcm1  15545  lcmfunsnlem2lem2  15574  lcmfunsnlem2  15575  prm2orodd  15625  phiprm  15702  pc0  15779  pcdvdstr  15800  vdwlem2  15906  vdwlem6  15910  vdwlem8  15912  hashbc0  15929  setsval  16102  fsets  16105  setsres  16115  ressinbas  16150  ressress  16153  elrestr  16297  pwssnf1o  16366  xpsfrnel  16431  ismred2  16471  submre  16473  mreacs  16526  oppchomfval  16581  brssc  16681  isssc  16687  yonedalem4c  17125  isprs  17138  oduleval  17339  oduclatb  17352  gsumval2a  17487  mulg1  17756  mulgnegnn  17759  isghm  17865  ghmghmrn  17884  cntrnsg  17978  oppgplusfval  17982  psgneldm2i  18129  efgrelexlemb  18367  frgp0  18377  frgpmhm  18382  vrgpf  18385  cygctb  18497  dprd0  18635  dprd2da  18646  mgpplusg  18698  opprmulfval  18830  subrgint  19009  lsp0  19219  sralem  19389  rlmval2  19406  fczpsrbag  19579  ply1idvr1  19874  evls1rhmlem  19897  evl1fval1lem  19905  zringcyg  20050  mulgrhm2  20058  zlmsca  20080  chrnzr  20089  zrhpsgnelbas  20151  ocvz  20236  cssincl  20246  css0  20247  css1  20248  frlmip  20331  marrepeval  20584  decpmatid  20792  0opn  20926  topopn  20928  basdif0  20975  tgval  20977  isopn2  21054  0cld  21060  ntropn  21071  ntrval2  21073  ntrdif  21074  clsdif  21075  cmclsopn  21084  clstop  21091  ntrtop  21092  cls0  21102  ntr0  21103  mretopd  21114  neips  21135  neiptopnei  21154  maxlp  21169  isperf2  21174  rest0  21191  iocpnfordt  21237  icomnfordt  21238  mnfnei  21243  refref  21534  unisngl  21548  1stckgen  21575  ptbasfi  21602  pthaus  21659  fbssfi  21858  isfil2  21877  ssfg  21893  filconn  21904  fbasrn  21905  filufint  21941  imaelfm  21972  fmfnfmlem4  21978  fclsfnflim  22048  alexsubALTlem3  22070  alexsubALTlem4  22071  ustfilxp  22233  ustuqtop2  22263  ustuqtop4  22265  utopsnneiplem  22268  utopsnnei  22270  utop2nei  22271  cfiluweak  22316  neipcfilu  22317  xmetres  22386  metres  22387  mopnex  22541  prdsms  22553  metucn  22593  tngds  22669  tngngp3  22677  nmoge0  22742  cnfldnm  22799  tgioo  22816  xrtgioo  22826  xrsmopn  22832  negcncf  22938  phtpy01  23001  pco0  23030  tchtopn  23241  tchnmfval  23243  caussi  23312  rrxip  23396  minveclem3b  23417  ovolfioo  23454  ovolficc  23455  ovolfsf  23458  ovolctb  23477  ovolctb2  23479  ovolfiniun  23488  ovoliun2  23493  ovolshftlem1  23496  ovolscalem1  23500  ovolicopnf  23511  iunmbl2  23544  uniioombllem2  23570  opnmblALT  23590  ismbf  23615  mbfinf  23652  0plef  23659  itg1climres  23701  itg2cnlem1  23748  iblitg  23755  ibl0  23773  itgcn  23829  cnlimc  23872  dvfre  23934  dvnfre  23935  dveflem  23962  dvef  23963  dvlipcn  23977  lhop2  23998  itgsubstlem  24031  deg1val  24076  ply1rem  24143  coefv0  24224  plyrecj  24255  vieta1lem2  24286  aannenlem1  24303  aaliou2b  24316  ulmval  24354  ulmpm  24357  ulmdvlem1  24374  mtest  24378  efcn  24417  sin2pim  24458  cos2pim  24459  sinmpi  24460  cosmpi  24461  sinppi  24462  cosppi  24463  efimpi  24464  sincosq1lem  24470  sincosq2sgn  24472  sincosq3sgn  24473  sincosq4sgn  24474  sinq12gt0  24480  sinq34lt0t  24482  sincosq1eq  24485  abssinper  24491  efif1o  24513  loglt1b  24600  relogcn  24604  ellogdm  24605  efopn  24624  cxp0  24636  cxp1  24637  cxpsqrt  24669  logsqrt  24670  logb1  24727  atandm3  24825  atanbnd  24873  atancn  24883  leibpi  24889  efrlim  24916  logdifbnd  24940  vmaprm  25063  ppip1le  25107  ppieq0  25122  prmorcht  25124  ppiublem1  25147  ppiub  25149  chpeq0  25153  chtub  25157  fsumvma  25158  pclogsum  25160  chpval2  25163  dchrresb  25204  dchrptlem1  25209  lgs0  25255  lgs2  25259  lgsdir2lem2  25271  lgsdir2lem4  25273  lgsdchrval  25299  lgsdchr  25300  lgseisenlem2  25321  2lgslem1c  25338  2lgsoddprmlem2  25354  dirith2  25437  selberg2lem  25459  qabvle  25534  qabvexp  25535  ostth  25548  istrkg2ld  25579  ttgval  25975  cchhllem  25987  brbtwn  25999  colinearalglem4  26009  upgr0eop  26229  uspgrushgr  26291  usgruspgr  26294  usgr0eop  26360  0grsubgr  26392  uspgrloopvtx  26645  umgr2v2evtx  26651  usgr0edg0rusgr  26705  rgrusgrprc  26719  wlkvtxiedg  26754  pthdivtx  26859  usgr2pthlem  26893  wlkswwlksf1o  27012  wwlksext2clwwlk  27213  wwlksext2clwwlkOLD  27214  konigsbergssiedgw  27429  frgrncvvdeqlem7  27486  2clwwlk2  27531  numclwwlk2lem1OLD  27569  ex-po  27629  pliguhgr  27675  nvnd  27877  ipval2lem3  27894  ipval2  27896  ipidsq  27899  dipcj  27903  dip0r  27906  nmlnogt0  27986  blocni  27994  ipasslem2  28021  ipasslem8  28026  ipasslem9  28027  ajval  28051  ubthlem1  28060  hvaddid2  28214  hvsub0  28267  hi02  28288  hlimi  28379  isch2  28414  chlimi  28425  chsupunss  28537  shsupunss  28539  chlejb1i  28669  h1dei  28743  h1de2ci  28749  spanunsni  28772  pjoml2i  28778  pjorthi  28862  mayete3i  28921  hosubid1  28991  nmopge0  29104  nmfnge0  29120  adj1  29126  adjeq  29128  lnop0  29159  lnopmi  29193  nmophmi  29224  cnlnadjlem5  29264  cnlnadjeui  29270  unierri  29297  leoprf2  29320  leopnmid  29331  nmopleid  29332  hstles  29424  hst0  29426  strlem3a  29445  dmdbr2  29496  mdsl1i  29514  mdsl2i  29515  mdsl2bi  29516  cvmdi  29517  mdslmd1lem1  29518  mdslmd1lem2  29519  mdslmd1i  29522  mdslmd2i  29523  csmdsymi  29527  mdexchi  29528  superpos  29547  atomli  29575  atordi  29577  chirredlem1  29583  chirredlem2  29584  atcvat4i  29590  atabsi  29594  mdsymlem1  29596  mdsymlem5  29600  mdsymlem6  29601  sumdmdii  29608  dmdbr5ati  29615  dmdbr6ati  29616  mddmdin0i  29624  cdj3lem2  29628  xppreima  29782  abfmpunirn  29785  abfmpel  29788  aciunf1lem  29795  fgreu  29804  imafi2  29822  padct  29830  fpwrelmapffslem  29840  fpwrelmap  29841  xrge0infss  29858  xrdifh  29875  clatp0cl  30002  clatp1cl  30003  resvval  30158  rearchi  30173  locfinreflem  30238  locfinref  30239  ordtconnlem1  30301  rge0scvg  30326  lmxrge0  30329  qqh0  30359  qqh1  30360  rrh0  30390  zrhre  30394  esumcst  30456  esumfzf  30462  esumfsupre  30464  hasheuni  30478  sgon  30518  dmvlsiga  30523  sigainb  30530  measval  30592  ismeas  30593  sxbrsigalem0  30664  omssubadd  30693  carsggect  30711  eulerpartlemmf  30768  eulerpartlemgs2  30773  eulerpartlemn  30774  rrvsum  30847  ballotlem2  30881  ballotlemfcc  30886  ballotlem4  30891  signsplypnf  30958  signsply0  30959  signsw0glem  30961  signswrid  30966  signlem0  30995  bnj535  31288  bnj580  31311  bnj907  31363  bnj1253  31413  ptpconn  31543  cvmsss2  31584  cvmlift2lem12  31624  cvmlift2lem13  31625  cvmliftphtlem  31627  cvmliftpht  31628  mppsthm  31804  bcneg1  31949  fprb  31996  fv1stcnv  32005  fv2ndcnv  32006  trpred0  32061  wlimeq1  32091  frr3g  32105  noextendseq  32146  noetalem3  32191  scutun12  32243  imagesset  32386  altopeq1  32396  brcolinear2  32491  gtinfOLD  32640  cldbnd  32647  ivthALT  32656  refssfne  32679  ontgval  32752  onint1  32770  axc11n11r  32993  bj-bm1.3ii  33336  bj-restsn10  33352  bj-restsnid  33353  bj-rest10  33354  bj-rest0  33359  bj-inftyexpiinv  33414  bj-inftyexpidisj  33416  taupilem1  33486  f1omptsnlem  33502  mptsnunlem  33504  topdifinffinlem  33513  finixpnum  33709  tan2h  33716  matunitlindflem2  33721  ptrest  33723  poimirlem22  33746  poimirlem25  33749  mblfinlem1  33761  mblfinlem2  33762  mblfinlem3  33763  mblfinlem4  33764  ismblfin  33765  itg2addnclem  33775  itg2addnclem2  33776  itg2addnclem3  33777  itg2addnc  33778  itg2gt0cn  33779  ftc1anclem5  33803  ftc1anclem8  33806  dvasin  33810  dvacos  33811  sdclem2  33851  totbndbnd  33901  heibor1lem  33921  heiborlem7  33929  bfplem1  33934  prnc  34179  brxrn  34451  riotasv  34740  glbconN  35159  atpointN  35525  polsubN  35689  pol0N  35691  pol1N  35692  2polvalN  35696  2polssN  35697  3polN  35698  pcl0N  35704  2pmaplubN  35708  pnonsingN  35715  polsubclN  35734  cdlemefs32sn1aw  36196  cdleme43fsv1snlem  36202  cdleme41sn3a  36215  cdleme32a  36223  cdleme40m  36249  cdleme40n  36250  cdleme42b  36260  istendo  36542  cdlemk40  36699  cdlemkid  36718  dihvalcqpre  37017  mapfzcons1cl  37784  eldioph3b  37831  eldiophss  37841  0dioph  37845  vdioph  37846  eldioph4b  37878  eldioph4i  37879  rencldnfilem  37887  rmxy1  37989  rmxy0  37990  rmxm1  38001  rmym1  38002  monotoddzzfi  38009  aomclem6  38131  pwslnmlem0  38163  isnumbasabl  38178  areaquad  38303  relexp2  38470  eltrclrec  38473  elrtrclrec  38474  brtrclrec  38489  brrtrclrec  38490  relexpxpmin  38510  dftrcl3  38513  dfrtrcl3  38526  heeq1  38572  seff  39009  lhe4.4ex1a  39029  eelT0  39500  snssl  39560  sineq0ALT  39668  elabrexg  39701  elrnmpt1sf  39866  founiiun0  39867  mapdm0OLD  39873  supxrgere  40030  supxrgelem  40034  fmuldfeqlem1  40295  fmuldfeq  40296  climneg  40323  sumnnodd  40343  liminfltlem  40517  addccncf2  40570  dvsinax  40608  stoweidlem18  40715  stoweidlem19  40716  stoweidlem22  40719  stoweidlem34  40731  stoweidlem40  40737  stoweidlem41  40738  stoweidlem55  40752  stoweidlem59  40756  dirker2re  40789  dirkerdenne0  40790  fourierdlem48  40851  fourierdlem49  40852  fourierdlem70  40873  fourierdlem71  40874  fourierdlem104  40907  fourierdlem112  40915  fouriersw  40928  etransclem46  40977  etransclem48  40979  nnfoctbdjlem  41152  fsummmodsnunz  41921  flsqrt5  42085  bits0ALTV  42166  mogoldbblem  42205  sgoldbeven3prm  42247  nnsum3primes4  42252  2zrngnmlid  42518  2zrngnmrid  42519  mpt2exxg2  42685  lco0  42785  zlmodzxzldeplem3  42860  0dig1  42972  aacllem  43119