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  3486  eueq2  3716  sbcgf  3861  sbcralg  3874  csbconstgf  3917  sbcnestgw  4423  csbnestgw  4424  sbcnestg  4428  csbnestg  4429  csbnest1g  4432  mpteq1OLD  5236  iinexg  5348  eusv2nf  5395  reusv2lem5  5402  nnullss  5467  xpss1  5704  xpiindi  5846  reldm0  5938  elrnmpt1s  5970  resdm  6044  eliniseg  6112  trinxp  6145  ssrnres  6198  cnveq0  6217  coi2  6283  relrelss  6293  cnviin  6306  elpred  6338  onelssex  6432  ord0eln0  6439  funcnvres  6644  funimaex  6655  fnresin1  6693  fnresin2  6694  fresin  6777  ssimaex  6994  fvmpt  7016  fvmptnf  7038  fvimacnvALT  7077  dff3  7120  fsn  7155  fsn2  7156  funop  7169  fvrnressn  7181  fninfp  7194  fndifnfp  7196  fnnfpeq0  7198  fprb  7214  elabrex  7262  elabrexg  7263  f1elima  7283  f1ofvswap  7326  fliftel1  7330  f1owe  7373  sorpssuni  7752  sorpssint  7753  eldifpw  7788  ordeleqon  7802  ordsson  7803  ssnlim  7907  abrexexg  7985  tposfun  8267  tpostpos2  8272  fpr3g  8310  wfr3g  8347  wfrlem14OLD  8362  wfrlem15OLD  8363  tfrlem10  8427  tfrlem12  8429  tfr3  8439  seqomlem1  8490  seqomlem2  8491  seqomlem4  8493  ondif2  8540  oa0  8554  om0  8555  oa1suc  8569  om1  8580  oe1  8582  oe1m  8583  omass  8618  oeoalem  8634  oeoelem  8636  nnmsucr  8663  nnm1  8690  nnm2  8691  naddrid  8721  naddlid  8722  ecelqsg  8812  xpider  8828  mapdm0  8882  fvdiagfn  8931  ixpsnf1o  8978  xp1en  9097  undom  9099  sbthlem7  9129  domunsn  9167  xpmapenlem  9184  infensuc  9195  findcard2d  9206  diffi  9215  cnvfi  9216  enreffi  9223  snnen2o  9273  1sdom2dom  9283  infi  9302  finresfin  9304  unblem1  9328  unblem2  9329  unblem3  9330  unblem4  9331  isfinite2  9334  infn0ALT  9341  unfilem1  9343  unfilem2  9344  unfir  9346  fofinf1o  9372  cnvfiALT  9379  mptfi  9391  finsschain  9399  marypha2  9479  inf0  9661  trcl  9768  frr3g  9796  r1rankidb  9844  snwf  9849  unwf  9850  uniwf  9859  rankval3b  9866  rankr1a  9876  rankxplim3  9921  scott0  9926  djueq1  9945  card1  10008  pm54.43  10041  infxpenc2  10062  dfac8clem  10072  alephsuc2  10120  alephle  10128  cardaleph  10129  dfac12lem2  10185  undjudom  10208  djudom1  10223  pwdju1  10231  nnadju  10238  ackbij1lem18  10276  cflem  10285  cflemOLD  10286  cflecard  10293  cfeq0  10296  cfslb  10306  cfsmolem  10310  cfcoflem  10312  cfidm  10315  isfin4p1  10355  fin23lem12  10371  fin23lem16  10375  fin23lem28  10380  fin23lem38  10389  fin23lem41  10392  fin1a2lem7  10446  fin1a2lem12  10451  fin1a2lem13  10452  hsmexlem8  10464  axcc2lem  10476  axcc3  10478  domtriomlem  10482  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  ac6num  10519  ttukeylem4  10552  ttukeylem7  10555  ttukey2g  10556  axdclem  10559  brdom3  10568  brdom5  10569  cardeq0  10592  unsnen  10593  konigthlem  10608  pwcfsdom  10623  canthp1lem1  10692  wunex2  10778  wuncval2  10787  eltsk2g  10791  ingru  10855  grutsk  10862  axgroth6  10868  mulidpi  10926  nlt1pi  10946  indpi  10947  pinq  10967  mulidnq  11003  1idpr  11069  prlem934  11073  0idsr  11137  1idsr  11138  00sr  11139  negexsr  11142  recexsrlem  11143  sqgt0sr  11146  ax1rid  11201  axcnre  11204  ne0gt0  11366  peano2cn  11433  peano2re  11434  00id  11436  mul02lem2  11438  mul01  11440  subid  11528  subid1  11529  negid  11556  negeq0  11563  peano2cnm  11575  peano2rem  11576  lt0neg1  11769  le0neg1  11771  relin01  11787  div2neg  11990  recgt0ii  12174  divgt0i2i  12183  ledivp1i  12193  ltdivp1i  12194  peano5nni  12269  peano2nn  12278  nnge1  12294  nnne0  12300  times2  12403  addltmul  12502  nn0p1nn  12565  peano2nn0  12566  nn0lele2xi  12582  fcdmnn0supp  12583  fcdmnn0fsupp  12584  fcdmnn0suppg  12585  peano2z  12658  peano2zm  12660  suprzcl  12698  zeo  12704  eluzaddi  12909  uzwo  12953  uzwo2  12954  infssuzle  12973  infssuzcl  12974  zq  12996  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  rphalfcl  13062  zgt1rpn0n1  13076  ltpnf  13162  nltmnf  13171  pnfge  13172  nltpnft  13206  xlemnf  13209  qsqueeze  13243  xlt0neg1  13261  xle0neg1  13263  xaddpnf1  13268  xaddmnf1  13270  xaddrid  13283  xsubge0  13303  xmul01  13309  xmulneg1  13311  xmulpnf1  13316  xmulrid  13321  supxrbnd  13370  supxrgtmnf  13371  supxrre1  13372  supxrre2  13373  elioopnf  13483  elicopnf  13485  iccshftri  13527  iccshftli  13529  iccdili  13531  icccntri  13533  fzprval  13625  fz0add1fz1  13774  fzofzp1  13803  fzostep1  13822  injresinj  13827  flge0nn0  13860  flge1nn  13861  btwnzge0  13868  modfrac  13924  om2uzsuci  13989  axdc4uzlem  14024  ser1const  14099  exp0  14106  exp1  14108  expn1  14112  nn0sqcl  14130  sqval  14155  sqeq0  14160  resqcl  14164  zsqcl  14169  expubnd  14217  binom21  14258  expnbnd  14271  nn0opthlem2  14308  bcnn  14351  bcn2  14358  bcn2p1  14364  bcnm1  14366  hasheq0  14402  hashsng  14408  hashen1  14409  hashunsnggt  14433  hashin  14450  hashdif  14452  hashgt23el  14463  hashxplem  14472  hashf1lem2  14495  hash2pr  14508  hash2prde  14509  pr2pwpr  14518  hash3tr  14530  iswrd  14554  wrdval  14555  hashwrdn  14585  ccatval2  14616  ccatrid  14625  eqs1  14650  s111  14653  ccatws1len  14658  repsw0  14815  repsw1  14821  cshw0  14832  wwlktovf  14995  relexpsucnnl  15069  reim0  15157  imval2  15190  cjne0  15202  abssq  15345  max0add  15349  abs2dif  15371  rddif  15379  absrdbnd  15380  rexuz3  15387  isershft  15700  isercolllem2  15702  isercoll  15704  fsum  15756  fsumadd  15776  fsumsplitsnun  15791  bcxmas  15871  infcvgaux2i  15894  fprod  15977  risefac0  16063  fallfac0  16064  risefac1  16069  fallfac1  16070  bpoly2  16093  bpoly3  16094  bpoly4  16095  fsumcube  16096  efi4p  16173  resin4p  16174  recos4p  16175  sinbnd  16216  cosbnd  16217  rpnnen2lem8  16257  rpnnen2lem12  16261  cnso  16283  dvdsmul2  16316  dvdslelem  16346  odd2np1lem  16377  mod2eq1n2dvds  16384  divalglem0  16430  divalglem1  16431  divalglem4  16433  divalglem5  16434  divalglem8  16437  flodddiv4  16452  bits0  16465  bitsp1o  16470  bitsf1  16483  sadadd2lem2  16487  gcd1  16565  lcm0val  16631  dvdslcm  16635  lcmeq0  16637  lcmgcd  16644  lcm1  16647  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  prm2orodd  16728  phiprm  16814  pc0  16892  pcdvdstr  16914  vdwlem2  17020  vdwlem6  17024  vdwlem8  17026  hashbc0  17043  setsval  17204  fsets  17206  setsres  17215  ressinbas  17291  ressress  17293  elrestr  17473  pwssnf1o  17543  xpsfrnel  17607  xpscf  17610  ismred2  17646  submre  17648  mreacs  17701  oppchomfval  17757  brssc  17858  isssc  17864  yonedalem4c  18322  oduleval  18334  isprs  18342  oduclatb  18552  gsumval2a  18698  smndex1n0mnd  18925  mulg1  19099  mulgnegnn  19102  isghmOLD  19234  ghmghmrn  19253  cntrnsg  19362  oppgplusfval  19366  pgrpsubgsymg  19427  psgneldm2i  19523  efgrelexlemb  19768  frgp0  19778  frgpmhm  19783  vrgpf  19786  cntrcmnd  19860  cntrabl  19861  cygctb  19910  dprd0  20051  dprd2da  20062  mgpplusg  20141  opprmulfval  20336  subrngint  20560  subrgint  20595  lsp0  21007  sralemOLD  21176  rlmval2  21199  cncrng  21401  cnfld1  21406  zringcyg  21480  mulgrhm2  21489  zlmsca  21535  fermltlchr  21544  chrnzr  21545  zrhpsgnelbas  21612  ocvz  21696  cssincl  21706  css0  21707  css1  21708  frlmip  21798  fczpsrbag  21941  ply1idvr1OLD  22299  evls1rhmlem  22325  evl1fval1lem  22334  marrepeval  22569  decpmatid  22776  0opn  22910  topopn  22912  basdif0  22960  tgval  22962  isopn2  23040  0cld  23046  ntropn  23057  ntrval2  23059  ntrdif  23060  clsdif  23061  cmclsopn  23070  ntrtop  23078  ntr0  23089  mretopd  23100  neips  23121  neiptopnei  23140  maxlp  23155  isperf2  23160  rest0  23177  iocpnfordt  23223  icomnfordt  23224  mnfnei  23229  refref  23521  unisngl  23535  1stckgen  23562  ptbasfi  23589  pthaus  23646  fbssfi  23845  isfil2  23864  ssfg  23880  filconn  23891  fbasrn  23892  filufint  23928  imaelfm  23959  fmfnfmlem4  23965  fclsfnflim  24035  alexsubALTlem3  24057  alexsubALTlem4  24058  ustfilxp  24221  ustuqtop2  24251  ustuqtop4  24253  utopsnneiplem  24256  utopsnnei  24258  utop2nei  24259  cfiluweak  24304  neipcfilu  24305  xmetres  24374  metres  24375  mopnex  24532  prdsms  24544  metucn  24584  tngds  24668  tngdsOLD  24669  tngngp3  24677  nmoge0  24742  cnfldnm  24799  tgioo  24817  xrtgioo  24828  xrsmopn  24834  negcncf  24948  negcncfOLD  24949  phtpy01  25017  pco0  25047  tcphtopn  25260  tchnmfval  25262  caussi  25331  rrxip  25424  minveclem3b  25462  ovolfioo  25502  ovolficc  25503  ovolfsf  25506  ovolctb  25525  ovolctb2  25527  ovolfiniun  25536  ovoliun2  25541  ovolshftlem1  25544  ovolscalem1  25548  ovolicopnf  25559  iunmbl2  25592  uniioombllem2  25618  opnmblALT  25638  ismbf  25663  mbfinf  25700  0plef  25707  itg1climres  25749  itg2cnlem1  25796  iblitg  25803  ibl0  25822  itgcn  25880  cnlimc  25923  dvfre  25989  dvnfre  25990  dveflem  26017  dvef  26018  dvlipcn  26033  lhop2  26054  itgsubstlem  26089  deg1val  26135  ply1rem  26205  coefv0  26287  plyrecj  26321  vieta1lem2  26353  aannenlem1  26370  aaliou2b  26383  ulmval  26423  ulmpm  26426  ulmdvlem1  26443  mtest  26447  efcn  26487  sin2pim  26527  cos2pim  26528  sinmpi  26529  cosmpi  26530  sinppi  26531  cosppi  26532  efimpi  26533  sincosq1lem  26539  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  sinq12gt0  26549  sinq34lt0t  26551  sincosq1eq  26554  abssinper  26563  efif1o  26588  loglt1b  26676  relogcn  26680  ellogdm  26681  efopn  26700  cxp0  26712  cxp1  26713  cxpsqrt  26745  logsqrt  26746  logb1  26812  atandm3  26921  atanbnd  26969  atancn  26979  leibpi  26985  efrlim  27012  efrlimOLD  27013  logdifbnd  27037  vmaprm  27160  ppip1le  27204  ppieq0  27219  prmorcht  27221  ppiublem1  27246  ppiub  27248  chpeq0  27252  chtub  27256  fsumvma  27257  pclogsum  27259  chpval2  27262  dchrresb  27303  dchrptlem1  27308  lgs0  27354  lgs2  27358  lgsdir2lem2  27370  lgsdir2lem4  27372  lgsdchrval  27398  lgsdchr  27399  lgseisenlem2  27420  2lgslem1c  27437  2lgsoddprmlem2  27453  addsq2nreurex  27488  dirith2  27572  selberg2lem  27594  qabvle  27669  qabvexp  27670  ostth  27683  noextendseq  27712  noetasuplem4  27781  noetainflem4  27785  scutun12  27855  madebdayim  27926  addsrid  27997  addsfo  28016  peano2no  28017  negscl  28068  subsfo  28095  subsid1  28098  muls01  28138  mulsrid  28139  divs1  28229  recsex  28243  abssnid  28267  peano2ons  28288  noseqp1  28297  noseqind  28298  peano2nns  28353  dfnns2  28362  elzs2  28385  elnnzs  28387  elznns  28388  n0seo  28405  exps0  28410  exps1  28411  istrkg2ld  28468  istrkg3ld  28469  ttgval  28883  ttgvalOLD  28884  cchhllemOLD  28902  brbtwn  28914  colinearalglem4  28924  upgr0eop  29131  uspgrushgr  29194  usgruspgr  29197  usgr0eop  29263  0grsubgr  29295  uspgrloopvtx  29533  umgr2v2evtx  29539  usgr0edg0rusgr  29593  rgrusgrprc  29607  wlkvtxiedg  29643  pthdivtx  29747  usgr2pthlem  29783  wlkswwlksf1o  29899  wwlksext2clwwlk  30076  konigsbergssiedgw  30269  frgrncvvdeqlem7  30324  2clwwlk2  30367  ex-po  30454  pliguhgr  30505  nvnd  30707  ipval2lem3  30724  ipval2  30726  ipidsq  30729  dipcj  30733  dip0r  30736  nmlnogt0  30816  blocni  30824  ipasslem2  30851  ipasslem8  30856  ipasslem9  30857  ajval  30880  ubthlem1  30889  hvaddlid  31042  hvsub0  31095  hi02  31116  hlimi  31207  isch2  31242  chlimi  31253  chsupunss  31363  shsupunss  31365  chlejb1i  31495  h1dei  31569  h1de2ci  31575  spanunsni  31598  pjoml2i  31604  pjorthi  31688  mayete3i  31747  hosubid1  31817  nmopge0  31930  nmfnge0  31946  adj1  31952  adjeq  31954  lnop0  31985  lnopmi  32019  nmophmi  32050  cnlnadjlem5  32090  cnlnadjeui  32096  unierri  32123  leoprf2  32146  leopnmid  32157  nmopleid  32158  hstles  32250  hst0  32252  strlem3a  32271  dmdbr2  32322  mdsl1i  32340  mdsl2i  32341  mdsl2bi  32342  cvmdi  32343  mdslmd1lem1  32344  mdslmd1lem2  32345  mdslmd1i  32348  mdslmd2i  32349  csmdsymi  32353  mdexchi  32354  superpos  32373  atomli  32401  atordi  32403  chirredlem1  32409  chirredlem2  32410  atcvat4i  32416  atabsi  32420  mdsymlem1  32422  mdsymlem5  32426  mdsymlem6  32427  sumdmdii  32434  dmdbr5ati  32441  dmdbr6ati  32442  mddmdin0i  32450  cdj3lem2  32454  unidifsnel  32553  unidifsnne  32554  xppreima  32655  abfmpunirn  32662  abfmpel  32665  aciunf1lem  32672  fgreu  32682  imafi2  32723  padct  32731  fpwrelmapffslem  32743  fpwrelmap  32744  xrge0infss  32764  xrdifh  32782  pfx1s2  32923  clatp0cl  32966  clatp1cl  32967  cntrcrng  33073  cycpmco2lem4  33149  rmfsupp2  33242  1fldgenq  33324  resvval  33353  rearchi  33374  qusxpid  33391  opprabs  33510  zringfrac  33582  rlmdim  33660  2sqr3minply  33791  locfinreflem  33839  locfinref  33840  ordtconnlem1  33923  rge0scvg  33948  lmxrge0  33951  qqh0  33985  qqh1  33986  rrh0  34016  zrhre  34020  esumcst  34064  esumfzf  34070  esumfsupre  34072  hasheuni  34086  sgon  34125  dmvlsiga  34130  sigainb  34137  measval  34199  ismeas  34200  sxbrsigalem0  34273  omssubadd  34302  carsggect  34320  eulerpartlemmf  34377  eulerpartlemgs2  34382  eulerpartlemn  34383  rrvsum  34456  ballotlem2  34491  ballotlemfcc  34496  ballotlem4  34501  signsplypnf  34565  signsply0  34566  signsw0glem  34568  signswrid  34573  signlem0  34602  signshf  34603  bnj535  34904  bnj580  34927  bnj907  34981  bnj1253  35031  funen1cnv  35102  loop1cycl  35142  ptpconn  35238  cvmsss2  35279  cvmlift2lem12  35319  cvmlift2lem13  35320  cvmliftphtlem  35322  cvmliftpht  35323  fmlafvel  35390  mppsthm  35584  bcneg1  35736  fv1stcnv  35777  fv2ndcnv  35778  wlimeq1  35821  imagesset  35954  altopeq1  35964  brcolinear2  36059  cldbnd  36327  ivthALT  36336  refssfne  36359  ontgval  36432  onint1  36450  axc11n11r  36684  bj-pm11.53a  36779  bj-bm1.3ii  37065  bj-restsn0  37086  bj-restsn10  37087  bj-restsnid  37088  bj-rest10  37089  bj-rest0  37094  bj-inftyexpiinv  37209  bj-inftyexpidisj  37211  taupilem1  37322  irrdiff  37327  f1omptsnlem  37337  mptsnunlem  37339  topdifinffinlem  37348  inunissunidif  37376  rdgssun  37379  exrecfnlem  37380  exrecfnpw  37382  finixpnum  37612  tan2h  37619  matunitlindflem2  37624  ptrest  37626  poimirlem22  37649  poimirlem25  37652  mblfinlem1  37664  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  itg2addnclem  37678  itg2addnclem2  37679  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  ftc1anclem5  37704  ftc1anclem8  37707  dvasin  37711  dvacos  37712  sdclem2  37749  totbndbnd  37796  heibor1lem  37816  heiborlem7  37824  bfplem1  37829  prnc  38074  ecexALTV  38332  brxrn  38375  riotasv  38960  glbconN  39378  glbconNOLD  39379  atpointN  39745  polsubN  39909  pol0N  39911  pol1N  39912  2polvalN  39916  2polssN  39917  3polN  39918  pcl0N  39924  2pmaplubN  39928  pnonsingN  39935  polsubclN  39954  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme41sn3a  40435  cdleme32a  40443  cdleme40m  40469  cdleme40n  40470  cdleme42b  40480  istendo  40762  cdlemk40  40919  cdlemkid  40938  dihvalcqpre  41237  facp2  42144  fac2xp3  42240  2xp3dxp2ge1d  42242  factwoffsmonot  42243  fnsnbt  42271  relt0neg1  42474  sn-nnne0  42478  sn-inelr  42497  frlmsnic  42550  prjspnerlem  42627  prjspnval2  42628  0prjspn  42638  3cubes  42701  mapfzcons1cl  42729  eldioph3b  42776  eldiophss  42785  0dioph  42789  vdioph  42790  eldioph4b  42822  eldioph4i  42823  rencldnfilem  42831  rmxy1  42934  rmxy0  42935  rmxm1  42946  rmym1  42947  monotoddzzfi  42954  wepwso  43055  aomclem6  43071  pwslnmlem0  43103  isnumbasabl  43118  areaquad  43228  onexlimgt  43255  oaabsb  43307  nadd1suc  43405  om2  43417  oe2  43419  safesnsupfidom1o  43430  onno  43446  oa1cl  43460  finona1cl  43466  reabsifneg  43645  reabsifnneg  43648  relexp2  43690  eltrclrec  43693  elrtrclrec  43694  brtrclrec  43709  brrtrclrec  43710  relexpxpmin  43730  dftrcl3  43733  dfrtrcl3  43746  heeq1  43790  seff  44328  lhe4.4ex1a  44348  eelT0  44795  snssl  44850  sineq0ALT  44957  trfr  44979  xpwf  44981  dmwf  44982  rnwf  44983  modelaxreplem1  44995  modelaxreplem3  44997  0elaxnul  45000  prclaxpr  45002  uniclaxun  45003  wfac8prim  45019  elrnmpt1sf  45194  founiiun0  45195  supxrgere  45344  supxrgelem  45348  fmuldfeqlem1  45597  fmuldfeq  45598  climneg  45625  sumnnodd  45645  liminfltlem  45819  xlimpnfxnegmnf2  45873  addccncf2  45891  dvsinax  45928  stoweidlem18  46033  stoweidlem19  46034  stoweidlem22  46037  stoweidlem34  46049  stoweidlem40  46055  stoweidlem41  46056  stoweidlem55  46070  stoweidlem59  46074  dirker2re  46107  dirkerdenne0  46108  fourierdlem48  46169  fourierdlem49  46170  fourierdlem70  46191  fourierdlem71  46192  fourierdlem104  46225  fourierdlem112  46233  fouriersw  46246  etransclem46  46295  etransclem48  46297  nnfoctbdjlem  46470  ormklocald  46889  natlocalincr  46891  singoutnword  46897  sqrtnegnre  47319  fsummmodsnunz  47362  flsqrt5  47581  bits0ALTV  47666  mogoldbblem  47707  sgoldbeven3prm  47770  nnsum3primes4  47775  isubgr0uhgr  47859  ushggricedg  47896  2zrngnmlid  48171  2zrngnmrid  48172  mpoexxg2  48254  lco0  48344  zlmodzxzldeplem3  48419  0dig1  48530  naryfvalel  48551  ackvalsuc0val  48608  0funclem  48919  aacllem  49320