Theorem mpan2 691

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 687	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanr12  705  mp3an23  1455  elvd  3453  elabg  3643  eueq2  3681  sbcgf  3824  sbcralg  3837  csbconstgf  3880  sbcnestgw  4386  csbnestgw  4387  sbcnestg  4391  csbnestg  4392  csbnest1g  4395  iinexg  5303  eusv2nf  5350  reusv2lem5  5357  nnullss  5422  xpss1  5657  xpiindi  5799  reldm0  5891  elrnmpt1s  5923  resdm  5997  eliniseg  6065  trinxp  6098  ssrnres  6151  cnveq0  6170  coi2  6236  relrelss  6246  cnviin  6259  elpred  6291  onelssex  6381  ord0eln0  6388  funcnvres  6594  funimaex  6605  fnresin1  6643  fnresin2  6644  fresin  6729  ssimaex  6946  fvmpt  6968  fvmptnf  6990  fvimacnvALT  7029  dff3  7072  fsn  7107  fsn2  7108  funop  7121  fvrnressn  7133  fnsnbg  7138  fninfp  7148  fndifnfp  7150  fnnfpeq0  7152  fprb  7168  elabrex  7216  elabrexg  7217  f1elima  7238  f1ofvswap  7281  fliftel1  7285  f1owe  7328  sorpssuni  7708  sorpssint  7709  eldifpw  7744  ordeleqon  7758  ordsson  7759  ssnlim  7862  abrexexg  7939  tposfun  8221  tpostpos2  8226  fpr3g  8264  wfr3g  8298  tfrlem10  8355  tfrlem12  8357  tfr3  8367  seqomlem1  8418  seqomlem2  8419  seqomlem4  8421  ondif2  8466  oa0  8480  om0  8481  oa1suc  8495  om1  8506  oe1  8508  oe1m  8509  omass  8544  oeoalem  8560  oeoelem  8562  nnmsucr  8589  nnm1  8616  nnm2  8617  naddrid  8647  naddlid  8648  ecelqs  8741  xpider  8761  mapdm0  8815  fvdiagfn  8864  ixpsnf1o  8911  xp1en  9027  undom  9029  sbthlem7  9057  domunsn  9091  xpmapenlem  9108  infensuc  9119  findcard2d  9130  diffi  9139  cnvfi  9140  enreffi  9147  snnen2o  9184  1sdom2dom  9194  infi  9213  finresfin  9215  unblem1  9239  unblem2  9240  unblem3  9241  unblem4  9242  isfinite2  9245  infn0ALT  9252  unfilem1  9254  unfilem2  9255  unfir  9257  fofinf1o  9283  cnvfiALT  9290  mptfi  9302  finsschain  9310  marypha2  9390  inf0  9574  trcl  9681  frr3g  9709  r1rankidb  9757  snwf  9762  unwf  9763  uniwf  9772  rankval3b  9779  rankr1a  9789  rankxplim3  9834  scott0  9839  djueq1  9858  card1  9921  pm54.43  9954  infxpenc2  9975  dfac8clem  9985  alephsuc2  10033  alephle  10041  cardaleph  10042  dfac12lem2  10098  undjudom  10121  djudom1  10136  pwdju1  10144  nnadju  10151  ackbij1lem18  10189  cflem  10198  cflemOLD  10199  cflecard  10206  cfeq0  10209  cfslb  10219  cfsmolem  10223  cfcoflem  10225  cfidm  10228  isfin4p1  10268  fin23lem12  10284  fin23lem16  10288  fin23lem28  10293  fin23lem38  10302  fin23lem41  10305  fin1a2lem7  10359  fin1a2lem12  10364  fin1a2lem13  10365  hsmexlem8  10377  axcc2lem  10389  axcc3  10391  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  ac6num  10432  ttukeylem4  10465  ttukeylem7  10468  ttukey2g  10469  axdclem  10472  brdom3  10481  brdom5  10482  cardeq0  10505  unsnen  10506  konigthlem  10521  pwcfsdom  10536  canthp1lem1  10605  wunex2  10691  wuncval2  10700  eltsk2g  10704  ingru  10768  grutsk  10775  axgroth6  10781  mulidpi  10839  nlt1pi  10859  indpi  10860  pinq  10880  mulidnq  10916  1idpr  10982  prlem934  10986  0idsr  11050  1idsr  11051  00sr  11052  negexsr  11055  recexsrlem  11056  sqgt0sr  11059  ax1rid  11114  axcnre  11117  ne0gt0  11279  peano2cn  11346  peano2re  11347  00id  11349  mul02lem2  11351  mul01  11353  subid  11441  subid1  11442  negid  11469  negeq0  11476  peano2cnm  11488  peano2rem  11489  lt0neg1  11684  le0neg1  11686  relin01  11702  div2neg  11905  recgt0ii  12089  divgt0i2i  12098  ledivp1i  12108  ltdivp1i  12109  inelr  12176  peano5nni  12189  peano2nn  12198  nnge1  12214  nnne0  12220  times2  12318  addltmul  12418  nn0p1nn  12481  peano2nn0  12482  nn0lele2xi  12498  fcdmnn0supp  12499  fcdmnn0fsupp  12500  fcdmnn0suppg  12501  peano2z  12574  peano2zm  12576  suprzcl  12614  zeo  12620  eluzaddi  12824  uzwo  12870  uzwo2  12871  infssuzle  12890  infssuzcl  12891  zq  12913  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  rphalfcl  12980  zgt1rpn0n1  12994  ltpnf  13080  nltmnf  13089  pnfge  13090  nltpnft  13124  xlemnf  13127  qsqueeze  13161  xlt0neg1  13179  xle0neg1  13181  xaddpnf1  13186  xaddmnf1  13188  xaddrid  13201  xsubge0  13221  xmul01  13227  xmulneg1  13229  xmulpnf1  13234  xmulrid  13239  supxrbnd  13288  supxrgtmnf  13289  supxrre1  13290  supxrre2  13291  elioopnf  13404  elicopnf  13406  iccshftri  13448  iccshftli  13450  iccdili  13452  icccntri  13454  fzprval  13546  fz0add1fz1  13696  fzofzp1  13725  fzostep1  13744  injresinj  13749  flge0nn0  13782  flge1nn  13783  btwnzge0  13790  modfrac  13846  om2uzsuci  13913  axdc4uzlem  13948  ser1const  14023  exp0  14030  exp1  14032  expn1  14036  nn0sqcl  14054  sqval  14079  sqeq0  14085  resqcl  14089  zsqcl  14094  expubnd  14143  binom21  14184  expnbnd  14197  nn0opthlem2  14234  bcnn  14277  bcn2  14284  bcn2p1  14290  bcnm1  14292  hasheq0  14328  hashsng  14334  hashen1  14335  hashunsnggt  14359  hashin  14376  hashdif  14378  hashgt23el  14389  hashxplem  14398  hashf1lem2  14421  hash2pr  14434  hash2prde  14435  pr2pwpr  14444  hash3tr  14456  iswrd  14480  wrdval  14481  hashwrdn  14512  ccatval2  14543  ccatrid  14552  eqs1  14577  s111  14580  ccatws1len  14585  repsw0  14742  repsw1  14748  cshw0  14759  wwlktovf  14922  relexpsucnnl  14996  reim0  15084  imval2  15117  cjne0  15129  abssq  15272  max0add  15276  abs2dif  15299  rddif  15307  absrdbnd  15308  rexuz3  15315  isershft  15630  isercolllem2  15632  isercoll  15634  fsum  15686  fsumadd  15706  fsumsplitsnun  15721  bcxmas  15801  infcvgaux2i  15824  fprod  15907  risefac0  15993  fallfac0  15994  risefac1  15999  fallfac1  16000  bpoly2  16023  bpoly3  16024  bpoly4  16025  fsumcube  16026  efi4p  16105  resin4p  16106  recos4p  16107  sinbnd  16148  cosbnd  16149  rpnnen2lem8  16189  rpnnen2lem12  16193  cnso  16215  dvdsmul2  16248  dvdslelem  16279  odd2np1lem  16310  mod2eq1n2dvds  16317  divalglem0  16363  divalglem1  16364  divalglem4  16366  divalglem5  16367  divalglem8  16370  flodddiv4  16385  bits0  16398  bitsp1o  16403  bitsf1  16416  sadadd2lem2  16420  gcd1  16498  lcm0val  16564  dvdslcm  16568  lcmeq0  16570  lcmgcd  16577  lcm1  16580  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  prm2orodd  16661  phiprm  16747  pc0  16825  pcdvdstr  16847  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  hashbc0  16976  setsval  17137  fsets  17139  setsres  17148  ressinbas  17215  ressress  17217  elrestr  17391  pwssnf1o  17461  xpsfrnel  17525  xpscf  17528  ismred2  17564  submre  17566  mreacs  17619  oppchomfval  17675  brssc  17776  isssc  17782  yonedalem4c  18238  oduleval  18250  isprs  18257  oduclatb  18466  gsumval2a  18612  smndex1n0mnd  18839  mulg1  19013  mulgnegnn  19016  isghmOLD  19148  ghmghmrn  19167  cntrnsg  19276  oppgplusfval  19280  pgrpsubgsymg  19339  psgneldm2i  19435  efgrelexlemb  19680  frgp0  19690  frgpmhm  19695  vrgpf  19698  cntrcmnd  19772  cntrabl  19773  cygctb  19822  dprd0  19963  dprd2da  19974  mgpplusg  20053  opprmulfval  20248  subrngint  20469  subrgint  20504  lsp0  20915  rlmval2  21099  cncrng  21300  cnfld1  21305  zringcyg  21379  mulgrhm2  21388  zlmsca  21430  fermltlchr  21439  chrnzr  21440  zrhpsgnelbas  21503  ocvz  21587  cssincl  21597  css0  21598  css1  21599  frlmip  21687  fczpsrbag  21830  ply1idvr1OLD  22182  evls1rhmlem  22208  evl1fval1lem  22217  marrepeval  22450  decpmatid  22657  0opn  22791  topopn  22793  basdif0  22840  tgval  22842  isopn2  22919  0cld  22925  ntropn  22936  ntrval2  22938  ntrdif  22939  clsdif  22940  cmclsopn  22949  ntrtop  22957  ntr0  22968  mretopd  22979  neips  23000  neiptopnei  23019  maxlp  23034  isperf2  23039  rest0  23056  iocpnfordt  23102  icomnfordt  23103  mnfnei  23108  refref  23400  unisngl  23414  1stckgen  23441  ptbasfi  23468  pthaus  23525  fbssfi  23724  isfil2  23743  ssfg  23759  filconn  23770  fbasrn  23771  filufint  23807  imaelfm  23838  fmfnfmlem4  23844  fclsfnflim  23914  alexsubALTlem3  23936  alexsubALTlem4  23937  ustfilxp  24100  ustuqtop2  24130  ustuqtop4  24132  utopsnneiplem  24135  utopsnnei  24137  utop2nei  24138  cfiluweak  24182  neipcfilu  24183  xmetres  24252  metres  24253  mopnex  24407  prdsms  24419  metucn  24459  tngds  24536  tngngp3  24544  nmoge0  24609  cnfldnm  24666  tgioo  24684  xrtgioo  24695  xrsmopn  24701  negcncf  24815  negcncfOLD  24816  phtpy01  24884  pco0  24914  tcphtopn  25126  tchnmfval  25128  caussi  25197  rrxip  25290  minveclem3b  25328  ovolfioo  25368  ovolficc  25369  ovolfsf  25372  ovolctb  25391  ovolctb2  25393  ovolfiniun  25402  ovoliun2  25407  ovolshftlem1  25410  ovolscalem1  25414  ovolicopnf  25425  iunmbl2  25458  uniioombllem2  25484  opnmblALT  25504  ismbf  25529  mbfinf  25566  0plef  25573  itg1climres  25615  itg2cnlem1  25662  iblitg  25669  ibl0  25688  itgcn  25746  cnlimc  25789  dvfre  25855  dvnfre  25856  dveflem  25883  dvef  25884  dvlipcn  25899  lhop2  25920  itgsubstlem  25955  deg1val  26001  ply1rem  26071  coefv0  26153  plyrecj  26187  vieta1lem2  26219  aannenlem1  26236  aaliou2b  26249  ulmval  26289  ulmpm  26292  ulmdvlem1  26309  mtest  26313  efcn  26353  sin2pim  26394  cos2pim  26395  sinmpi  26396  cosmpi  26397  sinppi  26398  cosppi  26399  efimpi  26400  sincosq1lem  26406  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  sinq12gt0  26416  sinq34lt0t  26418  sincosq1eq  26421  abssinper  26430  efif1o  26455  loglt1b  26543  relogcn  26547  ellogdm  26548  efopn  26567  cxp0  26579  cxp1  26580  cxpsqrt  26612  logsqrt  26613  logb1  26679  atandm3  26788  atanbnd  26836  atancn  26846  leibpi  26852  efrlim  26879  efrlimOLD  26880  logdifbnd  26904  vmaprm  27027  ppip1le  27071  ppieq0  27086  prmorcht  27088  ppiublem1  27113  ppiub  27115  chpeq0  27119  chtub  27123  fsumvma  27124  pclogsum  27126  chpval2  27129  dchrresb  27170  dchrptlem1  27175  lgs0  27221  lgs2  27225  lgsdir2lem2  27237  lgsdir2lem4  27239  lgsdchrval  27265  lgsdchr  27266  lgseisenlem2  27287  2lgslem1c  27304  2lgsoddprmlem2  27320  addsq2nreurex  27355  dirith2  27439  selberg2lem  27461  qabvle  27536  qabvexp  27537  ostth  27550  noextendseq  27579  noetasuplem4  27648  noetainflem4  27652  scutun12  27722  madebdayim  27799  addsrid  27871  addsfo  27890  peano2no  27891  negscl  27942  subsfo  27969  subsid1  27972  muls01  28015  mulsrid  28016  divs1  28107  recsex  28121  abssnid  28145  peano2ons  28176  noseqp1  28185  noseqind  28186  peano2nns  28242  n0sfincut  28246  dfnns2  28261  elzs2  28287  elnnzs  28289  elznns  28290  n0seo  28307  exps0  28313  exps1  28314  istrkg2ld  28387  istrkg3ld  28388  ttgval  28802  brbtwn  28826  colinearalglem4  28836  upgr0eop  29041  uspgrushgr  29104  usgruspgr  29107  usgr0eop  29173  0grsubgr  29205  uspgrloopvtx  29443  umgr2v2evtx  29449  usgr0edg0rusgr  29503  rgrusgrprc  29517  wlkvtxiedg  29553  pthdivtx  29657  usgr2pthlem  29693  wlkswwlksf1o  29809  wwlksext2clwwlk  29986  konigsbergssiedgw  30179  frgrncvvdeqlem7  30234  2clwwlk2  30277  ex-po  30364  pliguhgr  30415  nvnd  30617  ipval2lem3  30634  ipval2  30636  ipidsq  30639  dipcj  30643  dip0r  30646  nmlnogt0  30726  blocni  30734  ipasslem2  30761  ipasslem8  30766  ipasslem9  30767  ajval  30790  ubthlem1  30799  hvaddlid  30952  hvsub0  31005  hi02  31026  hlimi  31117  isch2  31152  chlimi  31163  chsupunss  31273  shsupunss  31275  chlejb1i  31405  h1dei  31479  h1de2ci  31485  spanunsni  31508  pjoml2i  31514  pjorthi  31598  mayete3i  31657  hosubid1  31727  nmopge0  31840  nmfnge0  31856  adj1  31862  adjeq  31864  lnop0  31895  lnopmi  31929  nmophmi  31960  cnlnadjlem5  32000  cnlnadjeui  32006  unierri  32033  leoprf2  32056  leopnmid  32067  nmopleid  32068  hstles  32160  hst0  32162  strlem3a  32181  dmdbr2  32232  mdsl1i  32250  mdsl2i  32251  mdsl2bi  32252  cvmdi  32253  mdslmd1lem1  32254  mdslmd1lem2  32255  mdslmd1i  32258  mdslmd2i  32259  csmdsymi  32263  mdexchi  32264  superpos  32283  atomli  32311  atordi  32313  chirredlem1  32319  chirredlem2  32320  atcvat4i  32326  atabsi  32330  mdsymlem1  32332  mdsymlem5  32336  mdsymlem6  32337  sumdmdii  32344  dmdbr5ati  32351  dmdbr6ati  32352  mddmdin0i  32360  cdj3lem2  32364  unidifsnel  32464  unidifsnne  32465  xppreima  32569  abfmpunirn  32576  abfmpel  32579  aciunf1lem  32586  fgreu  32596  imafi2  32635  padct  32643  fpwrelmapffslem  32655  fpwrelmap  32656  xrge0infss  32683  xrdifh  32703  pfx1s2  32860  clatp0cl  32902  clatp1cl  32903  cntrcrng  33010  cycpmco2lem4  33086  rmfsupp2  33189  1fldgenq  33272  resvval  33301  rearchi  33317  qusxpid  33334  opprabs  33453  zringfrac  33525  rlmdim  33605  constrfiss  33741  2sqr3minply  33770  locfinreflem  33830  locfinref  33831  ordtconnlem1  33914  rge0scvg  33939  lmxrge0  33942  qqh0  33974  qqh1  33975  rrh0  34005  zrhre  34009  esumcst  34053  esumfzf  34059  esumfsupre  34061  hasheuni  34075  sgon  34114  dmvlsiga  34119  sigainb  34126  measval  34188  ismeas  34189  sxbrsigalem0  34262  omssubadd  34291  carsggect  34309  eulerpartlemmf  34366  eulerpartlemgs2  34371  eulerpartlemn  34372  rrvsum  34445  ballotlem2  34480  ballotlemfcc  34485  ballotlem4  34490  signsplypnf  34541  signsply0  34542  signsw0glem  34544  signswrid  34549  signlem0  34578  signshf  34579  bnj535  34880  bnj580  34903  bnj907  34957  bnj1253  35007  funen1cnv  35078  onvf1odlem1  35090  onvf1od  35094  loop1cycl  35124  ptpconn  35220  cvmsss2  35261  cvmlift2lem12  35301  cvmlift2lem13  35302  cvmliftphtlem  35304  cvmliftpht  35305  fmlafvel  35372  mppsthm  35566  bcneg1  35723  fv1stcnv  35764  fv2ndcnv  35765  wlimeq1  35808  imagesset  35941  altopeq1  35951  brcolinear2  36046  cldbnd  36314  ivthALT  36323  refssfne  36346  ontgval  36419  onint1  36437  axc11n11r  36671  bj-pm11.53a  36766  bj-bm1.3ii  37052  bj-restsn0  37073  bj-restsn10  37074  bj-restsnid  37075  bj-rest10  37076  bj-rest0  37081  bj-inftyexpiinv  37196  bj-inftyexpidisj  37198  taupilem1  37309  irrdiff  37314  f1omptsnlem  37324  mptsnunlem  37326  topdifinffinlem  37335  inunissunidif  37363  rdgssun  37366  exrecfnlem  37367  exrecfnpw  37369  finixpnum  37599  tan2h  37606  matunitlindflem2  37611  ptrest  37613  poimirlem22  37636  poimirlem25  37639  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  ftc1anclem5  37691  ftc1anclem8  37694  dvasin  37698  dvacos  37699  sdclem2  37736  totbndbnd  37783  heibor1lem  37803  heiborlem7  37811  bfplem1  37816  prnc  38061  brxrn  38356  riotasv  38952  glbconN  39370  glbconNOLD  39371  atpointN  39737  polsubN  39901  pol0N  39903  pol1N  39904  2polvalN  39908  2polssN  39909  3polN  39910  pcl0N  39916  2pmaplubN  39920  pnonsingN  39927  polsubclN  39946  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme41sn3a  40427  cdleme32a  40435  cdleme40m  40461  cdleme40n  40462  cdleme42b  40472  istendo  40754  cdlemk40  40911  cdlemkid  40930  dihvalcqpre  41229  facp2  42131  relt0neg1  42444  sn-nnne0  42448  frlmsnic  42528  prjspnerlem  42605  prjspnval2  42606  0prjspn  42616  3cubes  42678  mapfzcons1cl  42706  eldioph3b  42753  eldiophss  42762  0dioph  42766  vdioph  42767  eldioph4b  42799  eldioph4i  42800  rencldnfilem  42808  rmxy1  42911  rmxy0  42912  rmxm1  42923  rmym1  42924  monotoddzzfi  42931  wepwso  43032  aomclem6  43048  pwslnmlem0  43080  isnumbasabl  43095  areaquad  43205  onexlimgt  43232  oaabsb  43283  nadd1suc  43381  om2  43393  oe2  43395  safesnsupfidom1o  43406  onno  43422  oa1cl  43436  finona1cl  43442  reabsifneg  43621  reabsifnneg  43624  relexp2  43666  eltrclrec  43669  elrtrclrec  43670  brtrclrec  43685  brrtrclrec  43686  relexpxpmin  43706  dftrcl3  43709  dfrtrcl3  43722  heeq1  43766  seff  44298  lhe4.4ex1a  44318  eelT0  44764  snssl  44819  sineq0ALT  44926  trfr  44952  xpwf  44954  dmwf  44955  rnwf  44956  modelaxreplem1  44968  modelaxreplem3  44970  0elaxnul  44973  prclaxpr  44975  uniclaxun  44976  wfac8prim  44992  permaxinf2lem  45002  elrnmpt1sf  45183  founiiun0  45184  supxrgere  45329  supxrgelem  45333  fmuldfeqlem1  45580  fmuldfeq  45581  climneg  45608  sumnnodd  45628  liminfltlem  45802  xlimpnfxnegmnf2  45856  addccncf2  45874  dvsinax  45911  stoweidlem18  46016  stoweidlem19  46017  stoweidlem22  46020  stoweidlem34  46032  stoweidlem40  46038  stoweidlem41  46039  stoweidlem55  46053  stoweidlem59  46057  dirker2re  46090  dirkerdenne0  46091  fourierdlem48  46152  fourierdlem49  46153  fourierdlem70  46174  fourierdlem71  46175  fourierdlem104  46208  fourierdlem112  46216  fouriersw  46229  etransclem46  46278  etransclem48  46280  nnfoctbdjlem  46453  ormklocald  46872  natlocalincr  46874  singoutnword  46880  cjnpoly  46890  sinnpoly  46892  sqrtnegnre  47308  fsummmodsnunz  47376  flsqrt5  47595  bits0ALTV  47680  mogoldbblem  47721  sgoldbeven3prm  47784  nnsum3primes4  47789  isubgr0uhgr  47873  ushggricedg  47927  2zrngnmlid  48243  2zrngnmrid  48244  mpoexxg2  48326  lco0  48416  zlmodzxzldeplem3  48491  0dig1  48598  naryfvalel  48619  ackvalsuc0val  48676  iinxp  48819  0funclem  49075  aacllem  49790