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

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  mpanr12  704  mp3an23  1454  elvd  3482  eueq2  3707  sbcgf  3855  sbcralg  3869  csbconstgf  3912  sbcnestgw  4421  csbnestgw  4422  sbcnestg  4426  csbnestg  4427  csbnest1g  4430  mpteq1OLD  5243  iinexg  5342  eusv2nf  5394  reusv2lem5  5401  nnullss  5463  xpss1  5696  xpiindi  5836  reldm0  5928  elrnmpt1s  5957  resdm  6027  eliniseg  6094  trinxp  6127  ssrnres  6178  cnveq0  6197  coi2  6263  relrelss  6273  cnviin  6286  elpred  6318  onelssex  6413  ord0eln0  6420  funcnvres  6627  funimaex  6637  fnresin1  6676  fnresin2  6677  fresin  6761  ssimaex  6977  fvmpt  6999  fvmptnf  7021  fvimacnvALT  7059  dff3  7102  fsn  7133  fsn2  7134  funop  7147  fvrnressn  7159  fninfp  7172  fndifnfp  7174  fnnfpeq0  7176  fprb  7195  elabrex  7242  f1elima  7262  f1ofvswap  7304  fliftel1  7307  f1owe  7350  sorpssuni  7722  sorpssint  7723  eldifpw  7755  ordeleqon  7769  ordsson  7770  ssnlim  7875  abrexexg  7947  tposfun  8227  tpostpos2  8232  fpr3g  8270  wfr3g  8307  wfrlem14OLD  8322  wfrlem15OLD  8323  tfrlem10  8387  tfrlem12  8389  tfr3  8399  seqomlem1  8450  seqomlem2  8451  seqomlem4  8453  ondif2  8502  oa0  8516  om0  8517  oa1suc  8531  om1  8542  oe1  8544  oe1m  8545  omass  8580  oeoalem  8596  oeoelem  8598  nnmsucr  8625  nnm1  8651  nnm2  8652  naddrid  8682  naddlid  8683  ecelqsg  8766  xpider  8782  mapdm0  8836  fvdiagfn  8885  ixpsnf1o  8932  xp1en  9057  undom  9059  sbthlem7  9089  domunsn  9127  xpmapenlem  9144  infensuc  9155  findcard2d  9166  diffi  9179  cnvfi  9180  enreffi  9186  snnen2o  9237  1sdom2dom  9247  infi  9268  finresfin  9270  unblem1  9295  unblem2  9296  unblem3  9297  unblem4  9298  isfinite2  9301  infn0ALT  9308  unfilem1  9310  unfilem2  9311  unfir  9314  fofinf1o  9327  cnvfiALT  9334  pwfilemOLD  9346  mptfi  9351  finsschain  9359  marypha2  9434  inf0  9616  trcl  9723  frr3g  9751  r1rankidb  9799  snwf  9804  unwf  9805  uniwf  9814  rankval3b  9821  rankr1a  9831  rankxplim3  9876  scott0  9881  djueq1  9900  card1  9963  pm54.43  9996  infxpenc2  10017  dfac8clem  10027  alephsuc2  10075  alephle  10083  cardaleph  10084  dfac12lem2  10139  undjudom  10162  djudom1  10177  pwdju1  10185  nnadju  10192  ackbij1lem18  10232  cflem  10241  cflecard  10248  cfeq0  10251  cfslb  10261  cfsmolem  10265  cfcoflem  10267  cfidm  10270  isfin4p1  10310  fin23lem12  10326  fin23lem16  10330  fin23lem28  10335  fin23lem38  10344  fin23lem41  10347  fin1a2lem7  10401  fin1a2lem12  10406  fin1a2lem13  10407  hsmexlem8  10419  axcc2lem  10431  axcc3  10433  domtriomlem  10437  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  ac6num  10474  ttukeylem4  10507  ttukeylem7  10510  ttukey2g  10511  axdclem  10514  brdom3  10523  brdom5  10524  cardeq0  10547  unsnen  10548  konigthlem  10563  pwcfsdom  10578  canthp1lem1  10647  wunex2  10733  wuncval2  10742  eltsk2g  10746  ingru  10810  grutsk  10817  axgroth6  10823  mulidpi  10881  nlt1pi  10901  indpi  10902  pinq  10922  mulidnq  10958  1idpr  11024  prlem934  11028  0idsr  11092  1idsr  11093  00sr  11094  negexsr  11097  recexsrlem  11098  sqgt0sr  11101  ax1rid  11156  axcnre  11159  ne0gt0  11319  peano2cn  11386  peano2re  11387  00id  11389  mul02lem2  11391  mul01  11393  subid  11479  subid1  11480  negid  11507  negeq0  11514  peano2cnm  11526  peano2rem  11527  lt0neg1  11720  le0neg1  11722  relin01  11738  div2neg  11937  recgt0ii  12120  divgt0i2i  12129  ledivp1i  12139  ltdivp1i  12140  peano5nni  12215  peano2nn  12224  nnge1  12240  nnne0  12246  times2  12349  addltmul  12448  nn0p1nn  12511  peano2nn0  12512  nn0lele2xi  12527  fcdmnn0supp  12528  fcdmnn0fsupp  12529  fcdmnn0suppg  12530  peano2z  12603  peano2zm  12605  suprzcl  12642  zeo  12648  eluzaddi  12853  uzwo  12895  uzwo2  12896  infssuzle  12915  infssuzcl  12916  zq  12938  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  rphalfcl  13001  zgt1rpn0n1  13015  ltpnf  13100  nltmnf  13109  pnfge  13110  nltpnft  13143  xlemnf  13146  qsqueeze  13180  xlt0neg1  13198  xle0neg1  13200  xaddpnf1  13205  xaddmnf1  13207  xaddrid  13220  xsubge0  13240  xmul01  13246  xmulneg1  13248  xmulpnf1  13253  xmulrid  13258  supxrbnd  13307  supxrgtmnf  13308  supxrre1  13309  supxrre2  13310  elioopnf  13420  elicopnf  13422  iccshftri  13464  iccshftli  13466  iccdili  13468  icccntri  13470  fzprval  13562  fz0add1fz1  13702  fzofzp1  13729  fzostep1  13748  injresinj  13753  flge0nn0  13785  flge1nn  13786  btwnzge0  13793  modfrac  13849  om2uzsuci  13913  axdc4uzlem  13948  ser1const  14024  exp0  14031  exp1  14033  expn1  14037  nn0sqcl  14055  sqval  14080  sqeq0  14085  resqcl  14089  zsqcl  14094  expubnd  14142  binom21  14182  expnbnd  14195  nn0opthlem2  14229  bcnn  14272  bcn2  14279  bcn2p1  14285  bcnm1  14287  hasheq0  14323  hashsng  14329  hashen1  14330  hashunsnggt  14354  hashin  14371  hashdif  14373  hashgt23el  14384  hashxplem  14393  hashf1lem2  14417  hash2pr  14430  hash2prde  14431  pr2pwpr  14440  hash3tr  14451  iswrd  14466  wrdval  14467  hashwrdn  14497  ccatval2  14528  ccatrid  14537  eqs1  14562  s111  14565  ccatws1len  14570  repsw0  14727  repsw1  14733  cshw0  14744  wwlktovf  14907  relexpsucnnl  14977  reim0  15065  imval2  15098  cjne0  15110  abssq  15253  max0add  15257  abs2dif  15279  rddif  15287  absrdbnd  15288  rexuz3  15295  isershft  15610  isercolllem2  15612  isercoll  15614  fsum  15666  fsumadd  15686  fsumsplitsnun  15701  bcxmas  15781  infcvgaux2i  15804  fprod  15885  risefac0  15971  fallfac0  15972  risefac1  15977  fallfac1  15978  bpoly2  16001  bpoly3  16002  bpoly4  16003  fsumcube  16004  efi4p  16080  resin4p  16081  recos4p  16082  sinbnd  16123  cosbnd  16124  rpnnen2lem8  16164  rpnnen2lem12  16168  cnso  16190  dvdsmul2  16222  dvdslelem  16252  odd2np1lem  16283  mod2eq1n2dvds  16290  divalglem0  16336  divalglem1  16337  divalglem4  16339  divalglem5  16340  divalglem8  16343  flodddiv4  16356  bits0  16369  bitsp1o  16374  bitsf1  16387  sadadd2lem2  16391  gcd1  16469  lcm0val  16531  dvdslcm  16535  lcmeq0  16537  lcmgcd  16544  lcm1  16547  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  prm2orodd  16628  phiprm  16710  pc0  16787  pcdvdstr  16809  vdwlem2  16915  vdwlem6  16919  vdwlem8  16921  hashbc0  16938  setsval  17100  fsets  17102  setsres  17111  ressinbas  17190  ressress  17193  elrestr  17374  pwssnf1o  17444  xpsfrnel  17508  xpscf  17511  ismred2  17547  submre  17549  mreacs  17602  oppchomfval  17658  oppchomfvalOLD  17659  brssc  17761  isssc  17767  yonedalem4c  18230  oduleval  18242  isprs  18250  oduclatb  18460  gsumval2a  18604  smndex1n0mnd  18793  mulg1  18961  mulgnegnn  18964  isghm  19092  ghmghmrn  19111  cntrnsg  19208  oppgplusfval  19212  pgrpsubgsymg  19277  psgneldm2i  19373  efgrelexlemb  19618  frgp0  19628  frgpmhm  19633  vrgpf  19636  cntrcmnd  19710  cntrabl  19711  cygctb  19760  dprd0  19901  dprd2da  19912  mgpplusg  19991  opprmulfval  20152  subrgint  20342  lsp0  20620  sralemOLD  20791  rlmval2  20816  zringcyg  21039  mulgrhm2  21048  zlmsca  21074  chrnzr  21082  zrhpsgnelbas  21147  ocvz  21231  cssincl  21241  css0  21242  css1  21243  frlmip  21333  fczpsrbag  21476  ply1idvr1  21817  evls1rhmlem  21840  evl1fval1lem  21849  marrepeval  22065  decpmatid  22272  0opn  22406  topopn  22408  basdif0  22456  tgval  22458  isopn2  22536  0cld  22542  ntropn  22553  ntrval2  22555  ntrdif  22556  clsdif  22557  cmclsopn  22566  ntrtop  22574  ntr0  22585  mretopd  22596  neips  22617  neiptopnei  22636  maxlp  22651  isperf2  22656  rest0  22673  iocpnfordt  22719  icomnfordt  22720  mnfnei  22725  refref  23017  unisngl  23031  1stckgen  23058  ptbasfi  23085  pthaus  23142  fbssfi  23341  isfil2  23360  ssfg  23376  filconn  23387  fbasrn  23388  filufint  23424  imaelfm  23455  fmfnfmlem4  23461  fclsfnflim  23531  alexsubALTlem3  23553  alexsubALTlem4  23554  ustfilxp  23717  ustuqtop2  23747  ustuqtop4  23749  utopsnneiplem  23752  utopsnnei  23754  utop2nei  23755  cfiluweak  23800  neipcfilu  23801  xmetres  23870  metres  23871  mopnex  24028  prdsms  24040  metucn  24080  tngds  24164  tngdsOLD  24165  tngngp3  24173  nmoge0  24238  cnfldnm  24295  tgioo  24312  xrtgioo  24322  xrsmopn  24328  negcncf  24438  phtpy01  24501  pco0  24530  tcphtopn  24743  tchnmfval  24745  caussi  24814  rrxip  24907  minveclem3b  24945  ovolfioo  24984  ovolficc  24985  ovolfsf  24988  ovolctb  25007  ovolctb2  25009  ovolfiniun  25018  ovoliun2  25023  ovolshftlem1  25026  ovolscalem1  25030  ovolicopnf  25041  iunmbl2  25074  uniioombllem2  25100  opnmblALT  25120  ismbf  25145  mbfinf  25182  0plef  25189  itg1climres  25232  itg2cnlem1  25279  iblitg  25286  ibl0  25304  itgcn  25362  cnlimc  25405  dvfre  25468  dvnfre  25469  dveflem  25496  dvef  25497  dvlipcn  25511  lhop2  25532  itgsubstlem  25565  deg1val  25614  ply1rem  25681  coefv0  25762  plyrecj  25793  vieta1lem2  25824  aannenlem1  25841  aaliou2b  25854  ulmval  25892  ulmpm  25895  ulmdvlem1  25912  mtest  25916  efcn  25955  sin2pim  25995  cos2pim  25996  sinmpi  25997  cosmpi  25998  sinppi  25999  cosppi  26000  efimpi  26001  sincosq1lem  26007  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  sinq12gt0  26017  sinq34lt0t  26019  sincosq1eq  26022  abssinper  26030  efif1o  26055  loglt1b  26142  relogcn  26146  ellogdm  26147  efopn  26166  cxp0  26178  cxp1  26179  cxpsqrt  26211  logsqrt  26212  logb1  26274  atandm3  26383  atanbnd  26431  atancn  26441  leibpi  26447  efrlim  26474  logdifbnd  26498  vmaprm  26621  ppip1le  26665  ppieq0  26680  prmorcht  26682  ppiublem1  26705  ppiub  26707  chpeq0  26711  chtub  26715  fsumvma  26716  pclogsum  26718  chpval2  26721  dchrresb  26762  dchrptlem1  26767  lgs0  26813  lgs2  26817  lgsdir2lem2  26829  lgsdir2lem4  26831  lgsdchrval  26857  lgsdchr  26858  lgseisenlem2  26879  2lgslem1c  26896  2lgsoddprmlem2  26912  addsq2nreurex  26947  dirith2  27031  selberg2lem  27053  qabvle  27128  qabvexp  27129  ostth  27142  noextendseq  27170  noetasuplem4  27239  noetainflem4  27243  scutun12  27311  madebdayim  27382  addsrid  27448  addsfo  27467  negscl  27510  subsid1  27536  muls01  27568  mulsrid  27569  divs1  27651  recsex  27665  istrkg2ld  27711  istrkg3ld  27712  ttgval  28126  ttgvalOLD  28127  cchhllemOLD  28145  brbtwn  28157  colinearalglem4  28167  upgr0eop  28374  uspgrushgr  28435  usgruspgr  28438  usgr0eop  28503  0grsubgr  28535  uspgrloopvtx  28772  umgr2v2evtx  28778  usgr0edg0rusgr  28832  rgrusgrprc  28846  wlkvtxiedg  28882  pthdivtx  28986  usgr2pthlem  29020  wlkswwlksf1o  29133  wwlksext2clwwlk  29310  konigsbergssiedgw  29503  frgrncvvdeqlem7  29558  2clwwlk2  29601  ex-po  29688  pliguhgr  29739  nvnd  29941  ipval2lem3  29958  ipval2  29960  ipidsq  29963  dipcj  29967  dip0r  29970  nmlnogt0  30050  blocni  30058  ipasslem2  30085  ipasslem8  30090  ipasslem9  30091  ajval  30114  ubthlem1  30123  hvaddlid  30276  hvsub0  30329  hi02  30350  hlimi  30441  isch2  30476  chlimi  30487  chsupunss  30597  shsupunss  30599  chlejb1i  30729  h1dei  30803  h1de2ci  30809  spanunsni  30832  pjoml2i  30838  pjorthi  30922  mayete3i  30981  hosubid1  31051  nmopge0  31164  nmfnge0  31180  adj1  31186  adjeq  31188  lnop0  31219  lnopmi  31253  nmophmi  31284  cnlnadjlem5  31324  cnlnadjeui  31330  unierri  31357  leoprf2  31380  leopnmid  31391  nmopleid  31392  hstles  31484  hst0  31486  strlem3a  31505  dmdbr2  31556  mdsl1i  31574  mdsl2i  31575  mdsl2bi  31576  cvmdi  31577  mdslmd1lem1  31578  mdslmd1lem2  31579  mdslmd1i  31582  mdslmd2i  31583  csmdsymi  31587  mdexchi  31588  superpos  31607  atomli  31635  atordi  31637  chirredlem1  31643  chirredlem2  31644  atcvat4i  31650  atabsi  31654  mdsymlem1  31656  mdsymlem5  31660  mdsymlem6  31661  sumdmdii  31668  dmdbr5ati  31675  dmdbr6ati  31676  mddmdin0i  31684  cdj3lem2  31688  unidifsnel  31772  unidifsnne  31773  xppreima  31871  abfmpunirn  31877  abfmpel  31880  aciunf1lem  31887  fgreu  31897  imafi2  31936  padct  31944  fpwrelmapffslem  31957  fpwrelmap  31958  xrge0infss  31973  xrdifh  31991  pfx1s2  32105  clatp0cl  32146  clatp1cl  32147  cntrcrng  32214  cycpmco2lem4  32288  rmfsupp2  32387  1fldgenq  32412  resvval  32441  rearchi  32461  qusxpid  32475  fermltlchr  32478  opprabs  32596  rlmdim  32694  locfinreflem  32820  locfinref  32821  ordtconnlem1  32904  rge0scvg  32929  lmxrge0  32932  qqh0  32964  qqh1  32965  rrh0  32995  zrhre  32999  esumcst  33061  esumfzf  33067  esumfsupre  33069  hasheuni  33083  sgon  33122  dmvlsiga  33127  sigainb  33134  measval  33196  ismeas  33197  sxbrsigalem0  33270  omssubadd  33299  carsggect  33317  eulerpartlemmf  33374  eulerpartlemgs2  33379  eulerpartlemn  33380  rrvsum  33453  ballotlem2  33487  ballotlemfcc  33492  ballotlem4  33497  signsplypnf  33561  signsply0  33562  signsw0glem  33564  signswrid  33569  signlem0  33598  signshf  33599  bnj535  33901  bnj580  33924  bnj907  33978  bnj1253  34028  funen1cnv  34091  loop1cycl  34128  ptpconn  34224  cvmsss2  34265  cvmlift2lem12  34305  cvmlift2lem13  34306  cvmliftphtlem  34308  cvmliftpht  34309  fmlafvel  34376  mppsthm  34570  bcneg1  34706  fv1stcnv  34748  fv2ndcnv  34749  wlimeq1  34792  imagesset  34925  altopeq1  34935  brcolinear2  35030  gg-negcncf  35166  cldbnd  35211  ivthALT  35220  refssfne  35243  ontgval  35316  onint1  35334  axc11n11r  35561  bj-pm11.53a  35656  bj-bm1.3ii  35945  bj-restsn0  35966  bj-restsn10  35967  bj-restsnid  35968  bj-rest10  35969  bj-rest0  35974  bj-inftyexpiinv  36089  bj-inftyexpidisj  36091  taupilem1  36202  irrdiff  36207  f1omptsnlem  36217  mptsnunlem  36219  topdifinffinlem  36228  inunissunidif  36256  rdgssun  36259  exrecfnlem  36260  exrecfnpw  36262  finixpnum  36473  tan2h  36480  matunitlindflem2  36485  ptrest  36487  poimirlem22  36510  poimirlem25  36513  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  itg2addnclem  36539  itg2addnclem2  36540  itg2addnclem3  36541  itg2addnc  36542  itg2gt0cn  36543  ftc1anclem5  36565  ftc1anclem8  36568  dvasin  36572  dvacos  36573  sdclem2  36610  totbndbnd  36657  heibor1lem  36677  heiborlem7  36685  bfplem1  36690  prnc  36935  ecexALTV  37200  brxrn  37244  riotasv  37829  glbconN  38247  glbconNOLD  38248  atpointN  38614  polsubN  38778  pol0N  38780  pol1N  38781  2polvalN  38785  2polssN  38786  3polN  38787  pcl0N  38793  2pmaplubN  38797  pnonsingN  38804  polsubclN  38823  cdlemefs32sn1aw  39285  cdleme43fsv1snlem  39291  cdleme41sn3a  39304  cdleme32a  39312  cdleme40m  39338  cdleme40n  39339  cdleme42b  39349  istendo  39631  cdlemk40  39788  cdlemkid  39807  dihvalcqpre  40106  facp2  40959  fac2xp3  41020  2xp3dxp2ge1d  41022  factwoffsmonot  41023  fnsnbt  41051  frlmsnic  41110  relt0neg1  41317  sn-nnne0  41321  sn-inelr  41338  prjspnerlem  41359  prjspnval2  41360  0prjspn  41370  3cubes  41428  mapfzcons1cl  41456  eldioph3b  41503  eldiophss  41512  0dioph  41516  vdioph  41517  eldioph4b  41549  eldioph4i  41550  rencldnfilem  41558  rmxy1  41661  rmxy0  41662  rmxm1  41673  rmym1  41674  monotoddzzfi  41681  wepwso  41785  aomclem6  41801  pwslnmlem0  41833  isnumbasabl  41848  areaquad  41965  onexlimgt  41992  oaabsb  42044  nadd1suc  42142  om2  42155  oe2  42157  safesnsupfidom1o  42168  onno  42184  oa1cl  42198  finona1cl  42204  reabsifneg  42383  reabsifnneg  42386  relexp2  42428  eltrclrec  42431  elrtrclrec  42432  brtrclrec  42447  brrtrclrec  42448  relexpxpmin  42468  dftrcl3  42471  dfrtrcl3  42484  heeq1  42528  seff  43068  lhe4.4ex1a  43088  eelT0  43536  snssl  43591  sineq0ALT  43698  elabrexg  43728  elrnmpt1sf  43887  founiiun0  43888  supxrgere  44043  supxrgelem  44047  fmuldfeqlem1  44298  fmuldfeq  44299  climneg  44326  sumnnodd  44346  liminfltlem  44520  xlimpnfxnegmnf2  44574  addccncf2  44592  dvsinax  44629  stoweidlem18  44734  stoweidlem19  44735  stoweidlem22  44738  stoweidlem34  44750  stoweidlem40  44756  stoweidlem41  44757  stoweidlem55  44771  stoweidlem59  44775  dirker2re  44808  dirkerdenne0  44809  fourierdlem48  44870  fourierdlem49  44871  fourierdlem70  44892  fourierdlem71  44893  fourierdlem104  44926  fourierdlem112  44934  fouriersw  44947  etransclem46  44996  etransclem48  44998  nnfoctbdjlem  45171  natlocalincr  45590  singoutnword  45596  upwrdfi  45601  sqrtnegnre  46015  fsummmodsnunz  46043  flsqrt5  46262  bits0ALTV  46347  mogoldbblem  46388  sgoldbeven3prm  46451  nnsum3primes4  46456  ushrisomgr  46509  subrngint  46739  2zrngnmlid  46847  2zrngnmrid  46848  mpoexxg2  47013  lco0  47108  zlmodzxzldeplem3  47183  0dig1  47295  naryfvalel  47316  ackvalsuc0val  47373  aacllem  47848