Theorem mpan2 688

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

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

This theorem is referenced by:  mpanr12  702  mp3an23  1452  elvd  3438  eueq2  3649  sbcgf  3798  sbcralg  3812  csbconstgf  3855  sbcnestgw  4360  csbnestgw  4361  sbcnestg  4365  csbnestg  4366  csbnest1g  4369  mpteq1OLD  5173  iinexg  5269  eusv2nf  5322  reusv2lem5  5329  nnullss  5381  xpss1  5609  xpiindi  5743  reldm0  5836  elrnmpt1s  5865  resdm  5935  eliniseg  6001  trinxp  6029  ssrnres  6080  cnveq0  6099  coi2  6166  relrelss  6175  cnviin  6188  elpred  6218  ord0eln0  6319  funcnvres  6510  funimaex  6519  fnresin1  6555  fnresin2  6556  fresin  6641  ssimaex  6850  fvmpt  6872  fvmptnf  6894  fvimacnvALT  6931  dff3  6973  fsn  7004  fsn2  7005  funop  7018  fvrnressn  7030  fninfp  7043  fndifnfp  7045  fnnfpeq0  7047  fprb  7066  elabrex  7113  f1elima  7133  f1ofvswap  7174  fliftel1  7177  f1owe  7220  sorpssuni  7579  sorpssint  7580  eldifpw  7612  ordeleqon  7626  ordsson  7627  ssnlim  7726  tposfun  8049  tpostpos2  8054  fpr3g  8092  wfr3g  8129  wfrlem14OLD  8144  wfrlem15OLD  8145  tfrlem10  8209  tfrlem12  8211  tfr3  8221  seqomlem1  8272  seqomlem2  8273  seqomlem4  8275  ondif2  8317  oa0  8331  om0  8332  oa1suc  8346  om1  8358  oe1  8360  oe1m  8361  omass  8396  oeoalem  8412  oeoelem  8414  nnmsucr  8441  nnm1  8465  nnm2  8466  ecelqsg  8544  xpider  8560  mapdm0  8613  fvdiagfn  8662  ixpsnf1o  8709  xp1en  8827  sbthlem7  8858  domunsn  8896  xpmapenlem  8913  infensuc  8924  findcard2d  8931  diffi  8944  cnvfi  8945  enreffi  8951  infi  9021  finresfin  9023  unblem1  9044  unblem2  9045  unblem3  9046  unblem4  9047  isfinite2  9050  infn0  9054  unfilem1  9056  unfilem2  9057  unfir  9060  fofinf1o  9072  cnvfiALT  9079  pwfilemOLD  9091  mptfi  9096  finsschain  9104  marypha2  9176  inf0  9357  trpred0  9479  trcl  9486  frr3g  9515  r1rankidb  9563  snwf  9568  unwf  9569  uniwf  9578  rankval3b  9585  rankr1a  9595  rankxplim3  9640  scott0  9645  djueq1  9664  card1  9727  pm54.43  9760  infxpenc2  9779  dfac8clem  9789  alephsuc2  9837  alephle  9845  cardaleph  9846  dfac12lem2  9901  undjudom  9924  djudom1  9939  pwdju1  9947  nnadju  9954  ackbij1lem18  9994  cflem  10003  cflecard  10010  cfeq0  10013  cfslb  10023  cfsmolem  10027  cfcoflem  10029  cfidm  10032  isfin4p1  10072  fin23lem12  10088  fin23lem16  10092  fin23lem28  10097  fin23lem38  10106  fin23lem41  10109  fin1a2lem7  10163  fin1a2lem12  10168  fin1a2lem13  10169  hsmexlem8  10181  axcc2lem  10193  axcc3  10195  domtriomlem  10199  axdc3lem2  10208  axdc3lem4  10210  axdc4lem  10212  axcclem  10214  ac6num  10236  ttukeylem4  10269  ttukeylem7  10272  ttukey2g  10273  axdclem  10276  brdom3  10285  brdom5  10286  cardeq0  10309  unsnen  10310  konigthlem  10325  pwcfsdom  10340  canthp1lem1  10409  wunex2  10495  wuncval2  10504  eltsk2g  10508  ingru  10572  grutsk  10579  axgroth6  10585  mulidpi  10643  nlt1pi  10663  indpi  10664  pinq  10684  mulidnq  10720  1idpr  10786  prlem934  10790  0idsr  10854  1idsr  10855  00sr  10856  negexsr  10859  recexsrlem  10860  sqgt0sr  10863  ax1rid  10918  axcnre  10921  ne0gt0  11080  peano2cn  11147  peano2re  11148  00id  11150  mul02lem2  11152  mul01  11154  subid  11240  subid1  11241  negid  11268  negeq0  11275  peano2cnm  11287  peano2rem  11288  lt0neg1  11481  le0neg1  11483  relin01  11499  div2neg  11698  recgt0ii  11881  divgt0i2i  11890  ledivp1i  11900  ltdivp1i  11901  peano5nni  11976  peano2nn  11985  nnge1  12001  times2  12110  addltmul  12209  nn0p1nn  12272  peano2nn0  12273  nn0lele2xi  12288  frnnn0supp  12289  frnnn0fsupp  12290  frnnn0suppg  12291  peano2z  12361  peano2zm  12363  suprzcl  12400  zeo  12406  uzwo  12650  uzwo2  12651  infssuzle  12670  infssuzcl  12671  zq  12693  rpnnen1lem1  12717  rpnnen1lem3  12718  rpnnen1lem5  12720  rphalfcl  12756  zgt1rpn0n1  12770  ltpnf  12855  nltmnf  12864  pnfge  12865  nltpnft  12897  xlemnf  12900  qsqueeze  12934  xlt0neg1  12952  xle0neg1  12954  xaddpnf1  12959  xaddmnf1  12961  xaddid1  12974  xsubge0  12994  xmul01  13000  xmulneg1  13002  xmulpnf1  13007  xmulid1  13012  supxrbnd  13061  supxrgtmnf  13062  supxrre1  13063  supxrre2  13064  elioopnf  13174  elicopnf  13176  iccshftri  13218  iccshftli  13220  iccdili  13222  icccntri  13224  fzprval  13316  fz0add1fz1  13455  fzofzp1  13482  fzostep1  13501  injresinj  13506  flge0nn0  13538  flge1nn  13539  btwnzge0  13546  modfrac  13602  om2uzsuci  13666  axdc4uzlem  13701  ser1const  13777  exp0  13784  exp1  13786  expn1  13790  nn0sqcl  13808  sqval  13833  sqeq0  13838  resqcl  13842  zsqcl  13846  expubnd  13893  binom21  13932  expnbnd  13945  nn0opthlem2  13981  bcnn  14024  bcn2  14031  bcn2p1  14037  bcnm1  14039  hasheq0  14076  hashsng  14082  hashen1  14083  hashunsnggt  14107  hashin  14124  hashdif  14126  hashgt23el  14137  hashxplem  14146  hashf1lem2  14168  hash2pr  14181  hash2prde  14182  pr2pwpr  14191  hash3tr  14202  iswrd  14217  wrdval  14218  hashwrdn  14248  ccatval2  14281  ccatrid  14290  eqs1  14315  s111  14318  ccatws1len  14323  repsw0  14488  repsw1  14494  cshw0  14505  wwlktovf  14669  relexpsucnnl  14739  reim0  14827  imval2  14860  cjne0  14872  abssq  15016  max0add  15020  abs2dif  15042  rddif  15050  absrdbnd  15051  rexuz3  15058  isershft  15373  isercolllem2  15375  isercoll  15377  fsum  15430  fsumadd  15450  fsumsplitsnun  15465  bcxmas  15545  infcvgaux2i  15568  fprod  15649  risefac0  15735  fallfac0  15736  risefac1  15741  fallfac1  15742  bpoly2  15765  bpoly3  15766  bpoly4  15767  fsumcube  15768  efi4p  15844  resin4p  15845  recos4p  15846  sinbnd  15887  cosbnd  15888  rpnnen2lem8  15928  rpnnen2lem12  15932  cnso  15954  dvdsmul2  15986  dvdslelem  16016  odd2np1lem  16047  mod2eq1n2dvds  16054  divalglem0  16100  divalglem1  16101  divalglem4  16103  divalglem5  16104  divalglem8  16107  flodddiv4  16120  bits0  16133  bitsp1o  16138  bitsf1  16151  sadadd2lem2  16155  gcd1  16233  gcdmultipleOLD  16258  lcm0val  16297  dvdslcm  16301  lcmeq0  16303  lcmgcd  16310  lcm1  16313  lcmfunsnlem2lem2  16342  lcmfunsnlem2  16343  prm2orodd  16394  phiprm  16476  pc0  16553  pcdvdstr  16575  vdwlem2  16681  vdwlem6  16685  vdwlem8  16687  hashbc0  16704  setsval  16866  fsets  16868  setsres  16877  ressinbas  16953  ressress  16956  elrestr  17137  pwssnf1o  17207  xpsfrnel  17271  xpscf  17274  ismred2  17310  submre  17312  mreacs  17365  oppchomfval  17421  oppchomfvalOLD  17422  brssc  17524  isssc  17530  yonedalem4c  17993  oduleval  18005  isprs  18013  oduclatb  18223  gsumval2a  18367  smndex1n0mnd  18549  mulg1  18709  mulgnegnn  18712  isghm  18832  ghmghmrn  18851  cntrnsg  18946  oppgplusfval  18950  pgrpsubgsymg  19015  psgneldm2i  19111  efgrelexlemb  19354  frgp0  19364  frgpmhm  19369  vrgpf  19372  cntrcmnd  19441  cntrabl  19442  cygctb  19491  dprd0  19632  dprd2da  19643  mgpplusg  19722  opprmulfval  19862  subrgint  20044  lsp0  20269  sralemOLD  20438  rlmval2  20462  zringcyg  20689  mulgrhm2  20698  zlmsca  20724  chrnzr  20732  zrhpsgnelbas  20797  ocvz  20881  cssincl  20891  css0  20892  css1  20893  frlmip  20983  fczpsrbag  21124  ply1idvr1  21462  evls1rhmlem  21485  evl1fval1lem  21494  marrepeval  21710  decpmatid  21917  0opn  22051  topopn  22053  basdif0  22101  tgval  22103  isopn2  22181  0cld  22187  ntropn  22198  ntrval2  22200  ntrdif  22201  clsdif  22202  cmclsopn  22211  ntrtop  22219  ntr0  22230  mretopd  22241  neips  22262  neiptopnei  22281  maxlp  22296  isperf2  22301  rest0  22318  iocpnfordt  22364  icomnfordt  22365  mnfnei  22370  refref  22662  unisngl  22676  1stckgen  22703  ptbasfi  22730  pthaus  22787  fbssfi  22986  isfil2  23005  ssfg  23021  filconn  23032  fbasrn  23033  filufint  23069  imaelfm  23100  fmfnfmlem4  23106  fclsfnflim  23176  alexsubALTlem3  23198  alexsubALTlem4  23199  ustfilxp  23362  ustuqtop2  23392  ustuqtop4  23394  utopsnneiplem  23397  utopsnnei  23399  utop2nei  23400  cfiluweak  23445  neipcfilu  23446  xmetres  23515  metres  23516  mopnex  23673  prdsms  23685  metucn  23725  tngds  23809  tngdsOLD  23810  tngngp3  23818  nmoge0  23883  cnfldnm  23940  tgioo  23957  xrtgioo  23967  xrsmopn  23973  negcncf  24083  phtpy01  24146  pco0  24175  tcphtopn  24388  tchnmfval  24390  caussi  24459  rrxip  24552  minveclem3b  24590  ovolfioo  24629  ovolficc  24630  ovolfsf  24633  ovolctb  24652  ovolctb2  24654  ovolfiniun  24663  ovoliun2  24668  ovolshftlem1  24671  ovolscalem1  24675  ovolicopnf  24686  iunmbl2  24719  uniioombllem2  24745  opnmblALT  24765  ismbf  24790  mbfinf  24827  0plef  24834  itg1climres  24877  itg2cnlem1  24924  iblitg  24931  ibl0  24949  itgcn  25007  cnlimc  25050  dvfre  25113  dvnfre  25114  dveflem  25141  dvef  25142  dvlipcn  25156  lhop2  25177  itgsubstlem  25210  deg1val  25259  ply1rem  25326  coefv0  25407  plyrecj  25438  vieta1lem2  25469  aannenlem1  25486  aaliou2b  25499  ulmval  25537  ulmpm  25540  ulmdvlem1  25557  mtest  25561  efcn  25600  sin2pim  25640  cos2pim  25641  sinmpi  25642  cosmpi  25643  sinppi  25644  cosppi  25645  efimpi  25646  sincosq1lem  25652  sincosq2sgn  25654  sincosq3sgn  25655  sincosq4sgn  25656  sinq12gt0  25662  sinq34lt0t  25664  sincosq1eq  25667  abssinper  25675  efif1o  25700  loglt1b  25787  relogcn  25791  ellogdm  25792  efopn  25811  cxp0  25823  cxp1  25824  cxpsqrt  25856  logsqrt  25857  logb1  25917  atandm3  26026  atanbnd  26074  atancn  26084  leibpi  26090  efrlim  26117  logdifbnd  26141  vmaprm  26264  ppip1le  26308  ppieq0  26323  prmorcht  26325  ppiublem1  26348  ppiub  26350  chpeq0  26354  chtub  26358  fsumvma  26359  pclogsum  26361  chpval2  26364  dchrresb  26405  dchrptlem1  26410  lgs0  26456  lgs2  26460  lgsdir2lem2  26472  lgsdir2lem4  26474  lgsdchrval  26500  lgsdchr  26501  lgseisenlem2  26522  2lgslem1c  26539  2lgsoddprmlem2  26555  addsq2nreurex  26590  dirith2  26674  selberg2lem  26696  qabvle  26771  qabvexp  26772  ostth  26785  istrkg2ld  26819  istrkg3ld  26820  ttgval  27234  ttgvalOLD  27235  cchhllemOLD  27253  brbtwn  27265  colinearalglem4  27275  upgr0eop  27482  uspgrushgr  27543  usgruspgr  27546  usgr0eop  27611  0grsubgr  27643  uspgrloopvtx  27880  umgr2v2evtx  27886  usgr0edg0rusgr  27940  rgrusgrprc  27954  wlkvtxiedg  27989  pthdivtx  28093  usgr2pthlem  28127  wlkswwlksf1o  28240  wwlksext2clwwlk  28417  konigsbergssiedgw  28610  frgrncvvdeqlem7  28665  2clwwlk2  28708  ex-po  28795  pliguhgr  28844  nvnd  29046  ipval2lem3  29063  ipval2  29065  ipidsq  29068  dipcj  29072  dip0r  29075  nmlnogt0  29155  blocni  29163  ipasslem2  29190  ipasslem8  29195  ipasslem9  29196  ajval  29219  ubthlem1  29228  hvaddid2  29381  hvsub0  29434  hi02  29455  hlimi  29546  isch2  29581  chlimi  29592  chsupunss  29702  shsupunss  29704  chlejb1i  29834  h1dei  29908  h1de2ci  29914  spanunsni  29937  pjoml2i  29943  pjorthi  30027  mayete3i  30086  hosubid1  30156  nmopge0  30269  nmfnge0  30285  adj1  30291  adjeq  30293  lnop0  30324  lnopmi  30358  nmophmi  30389  cnlnadjlem5  30429  cnlnadjeui  30435  unierri  30462  leoprf2  30485  leopnmid  30496  nmopleid  30497  hstles  30589  hst0  30591  strlem3a  30610  dmdbr2  30661  mdsl1i  30679  mdsl2i  30680  mdsl2bi  30681  cvmdi  30682  mdslmd1lem1  30683  mdslmd1lem2  30684  mdslmd1i  30687  mdslmd2i  30688  csmdsymi  30692  mdexchi  30693  superpos  30712  atomli  30740  atordi  30742  chirredlem1  30748  chirredlem2  30749  atcvat4i  30755  atabsi  30759  mdsymlem1  30761  mdsymlem5  30765  mdsymlem6  30766  sumdmdii  30773  dmdbr5ati  30780  dmdbr6ati  30781  mddmdin0i  30789  cdj3lem2  30793  unidifsnel  30879  unidifsnne  30880  xppreima  30979  abfmpunirn  30985  abfmpel  30988  aciunf1lem  30995  fgreu  31005  imafi2  31042  padct  31050  fpwrelmapffslem  31063  fpwrelmap  31064  xrge0infss  31079  xrdifh  31097  pfx1s2  31209  clatp0cl  31250  clatp1cl  31251  cntrcrng  31318  cycpmco2lem4  31392  rmfsupp2  31488  resvval  31522  rearchi  31542  qusxpid  31555  locfinreflem  31786  locfinref  31787  ordtconnlem1  31870  rge0scvg  31895  lmxrge0  31898  qqh0  31930  qqh1  31931  rrh0  31961  zrhre  31965  esumcst  32027  esumfzf  32033  esumfsupre  32035  hasheuni  32049  sgon  32088  dmvlsiga  32093  sigainb  32100  measval  32162  ismeas  32163  sxbrsigalem0  32234  omssubadd  32263  carsggect  32281  eulerpartlemmf  32338  eulerpartlemgs2  32343  eulerpartlemn  32344  rrvsum  32417  ballotlem2  32451  ballotlemfcc  32456  ballotlem4  32461  signsplypnf  32525  signsply0  32526  signsw0glem  32528  signswrid  32533  signlem0  32562  signshf  32563  bnj535  32866  bnj580  32889  bnj907  32943  bnj1253  32993  funen1cnv  33056  loop1cycl  33095  ptpconn  33191  cvmsss2  33232  cvmlift2lem12  33272  cvmlift2lem13  33273  cvmliftphtlem  33275  cvmliftpht  33276  fmlafvel  33343  mppsthm  33537  onelssex  33657  bcneg1  33698  fv1stcnv  33747  fv2ndcnv  33748  wlimeq1  33810  naddid1  33832  noextendseq  33866  noetasuplem4  33935  noetainflem4  33939  scutun12  34000  madebdayim  34066  addsid1  34123  imagesset  34251  altopeq1  34261  brcolinear2  34356  cldbnd  34511  ivthALT  34520  refssfne  34543  ontgval  34616  onint1  34634  axc11n11r  34861  bj-pm11.53a  34956  bj-bm1.3ii  35231  bj-restsn0  35252  bj-restsn10  35253  bj-restsnid  35254  bj-rest10  35255  bj-rest0  35260  bj-inftyexpiinv  35375  bj-inftyexpidisj  35377  taupilem1  35488  irrdiff  35493  f1omptsnlem  35503  mptsnunlem  35505  topdifinffinlem  35514  inunissunidif  35542  rdgssun  35545  exrecfnlem  35546  exrecfnpw  35548  finixpnum  35758  tan2h  35765  matunitlindflem2  35770  ptrest  35772  poimirlem22  35795  poimirlem25  35798  mblfinlem1  35810  mblfinlem2  35811  mblfinlem3  35812  mblfinlem4  35813  ismblfin  35814  itg2addnclem  35824  itg2addnclem2  35825  itg2addnclem3  35826  itg2addnc  35827  itg2gt0cn  35828  ftc1anclem5  35850  ftc1anclem8  35853  dvasin  35857  dvacos  35858  sdclem2  35896  totbndbnd  35943  heibor1lem  35963  heiborlem7  35971  bfplem1  35976  prnc  36221  ecexALTV  36462  brxrn  36500  riotasv  36969  glbconN  37387  atpointN  37753  polsubN  37917  pol0N  37919  pol1N  37920  2polvalN  37924  2polssN  37925  3polN  37926  pcl0N  37932  2pmaplubN  37936  pnonsingN  37943  polsubclN  37962  cdlemefs32sn1aw  38424  cdleme43fsv1snlem  38430  cdleme41sn3a  38443  cdleme32a  38451  cdleme40m  38477  cdleme40n  38478  cdleme42b  38488  istendo  38770  cdlemk40  38927  cdlemkid  38946  dihvalcqpre  39245  facp2  40096  fac2xp3  40157  2xp3dxp2ge1d  40159  factwoffsmonot  40160  fnsnbt  40205  frlmsnic  40260  relt0neg1  40422  sn-inelr  40432  prjspnerlem  40453  prjspnval2  40454  0prjspn  40462  3cubes  40509  mapfzcons1cl  40537  eldioph3b  40584  eldiophss  40593  0dioph  40597  vdioph  40598  eldioph4b  40630  eldioph4i  40631  rencldnfilem  40639  rmxy1  40741  rmxy0  40742  rmxm1  40753  rmym1  40754  monotoddzzfi  40761  wepwso  40865  aomclem6  40881  pwslnmlem0  40913  isnumbasabl  40928  areaquad  41044  reabsifneg  41210  reabsifnneg  41213  relexp2  41255  eltrclrec  41258  elrtrclrec  41259  brtrclrec  41274  brrtrclrec  41275  relexpxpmin  41295  dftrcl3  41298  dfrtrcl3  41311  heeq1  41355  seff  41897  lhe4.4ex1a  41917  eelT0  42365  snssl  42420  sineq0ALT  42527  elabrexg  42559  elrnmpt1sf  42697  founiiun0  42698  supxrgere  42843  supxrgelem  42847  fmuldfeqlem1  43094  fmuldfeq  43095  climneg  43122  sumnnodd  43142  liminfltlem  43316  xlimpnfxnegmnf2  43370  addccncf2  43388  dvsinax  43425  stoweidlem18  43530  stoweidlem19  43531  stoweidlem22  43534  stoweidlem34  43546  stoweidlem40  43552  stoweidlem41  43553  stoweidlem55  43567  stoweidlem59  43571  dirker2re  43604  dirkerdenne0  43605  fourierdlem48  43666  fourierdlem49  43667  fourierdlem70  43688  fourierdlem71  43689  fourierdlem104  43722  fourierdlem112  43730  fouriersw  43743  etransclem46  43792  etransclem48  43794  nnfoctbdjlem  43964  sqrtnegnre  44768  fsummmodsnunz  44796  flsqrt5  45015  bits0ALTV  45100  mogoldbblem  45141  sgoldbeven3prm  45204  nnsum3primes4  45209  ushrisomgr  45262  2zrngnmlid  45476  2zrngnmrid  45477  mpoexxg2  45642  lco0  45737  zlmodzxzldeplem3  45812  0dig1  45924  naryfvalel  45945  ackvalsuc0val  46002  aacllem  46474