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  1454  elvd  3469  eueq2  3698  sbcgf  3841  sbcralg  3854  csbconstgf  3897  sbcnestgw  4403  csbnestgw  4404  sbcnestg  4408  csbnestg  4409  csbnest1g  4412  mpteq1OLD  5216  iinexg  5328  eusv2nf  5375  reusv2lem5  5382  nnullss  5447  xpss1  5684  xpiindi  5826  reldm0  5918  elrnmpt1s  5950  resdm  6024  eliniseg  6092  trinxp  6125  ssrnres  6178  cnveq0  6197  coi2  6263  relrelss  6273  cnviin  6286  elpred  6318  onelssex  6412  ord0eln0  6419  funcnvres  6624  funimaex  6635  fnresin1  6673  fnresin2  6674  fresin  6757  ssimaex  6974  fvmpt  6996  fvmptnf  7018  fvimacnvALT  7057  dff3  7100  fsn  7135  fsn2  7136  funop  7149  fvrnressn  7161  fnsnbg  7166  fninfp  7176  fndifnfp  7178  fnnfpeq0  7180  fprb  7196  elabrex  7244  elabrexg  7245  f1elima  7265  f1ofvswap  7308  fliftel1  7312  f1owe  7355  sorpssuni  7734  sorpssint  7735  eldifpw  7770  ordeleqon  7784  ordsson  7785  ssnlim  7889  abrexexg  7967  tposfun  8249  tpostpos2  8254  fpr3g  8292  wfr3g  8329  wfrlem14OLD  8344  wfrlem15OLD  8345  tfrlem10  8409  tfrlem12  8411  tfr3  8421  seqomlem1  8472  seqomlem2  8473  seqomlem4  8475  ondif2  8522  oa0  8536  om0  8537  oa1suc  8551  om1  8562  oe1  8564  oe1m  8565  omass  8600  oeoalem  8616  oeoelem  8618  nnmsucr  8645  nnm1  8672  nnm2  8673  naddrid  8703  naddlid  8704  ecelqsg  8794  xpider  8810  mapdm0  8864  fvdiagfn  8913  ixpsnf1o  8960  xp1en  9079  undom  9081  sbthlem7  9111  domunsn  9149  xpmapenlem  9166  infensuc  9177  findcard2d  9188  diffi  9197  cnvfi  9198  enreffi  9205  snnen2o  9255  1sdom2dom  9265  infi  9284  finresfin  9286  unblem1  9310  unblem2  9311  unblem3  9312  unblem4  9313  isfinite2  9316  infn0ALT  9323  unfilem1  9325  unfilem2  9326  unfir  9328  fofinf1o  9354  cnvfiALT  9361  mptfi  9373  finsschain  9381  marypha2  9461  inf0  9643  trcl  9750  frr3g  9778  r1rankidb  9826  snwf  9831  unwf  9832  uniwf  9841  rankval3b  9848  rankr1a  9858  rankxplim3  9903  scott0  9908  djueq1  9927  card1  9990  pm54.43  10023  infxpenc2  10044  dfac8clem  10054  alephsuc2  10102  alephle  10110  cardaleph  10111  dfac12lem2  10167  undjudom  10190  djudom1  10205  pwdju1  10213  nnadju  10220  ackbij1lem18  10258  cflem  10267  cflemOLD  10268  cflecard  10275  cfeq0  10278  cfslb  10288  cfsmolem  10292  cfcoflem  10294  cfidm  10297  isfin4p1  10337  fin23lem12  10353  fin23lem16  10357  fin23lem28  10362  fin23lem38  10371  fin23lem41  10374  fin1a2lem7  10428  fin1a2lem12  10433  fin1a2lem13  10434  hsmexlem8  10446  axcc2lem  10458  axcc3  10460  domtriomlem  10464  axdc3lem2  10473  axdc3lem4  10475  axdc4lem  10477  axcclem  10479  ac6num  10501  ttukeylem4  10534  ttukeylem7  10537  ttukey2g  10538  axdclem  10541  brdom3  10550  brdom5  10551  cardeq0  10574  unsnen  10575  konigthlem  10590  pwcfsdom  10605  canthp1lem1  10674  wunex2  10760  wuncval2  10769  eltsk2g  10773  ingru  10837  grutsk  10844  axgroth6  10850  mulidpi  10908  nlt1pi  10928  indpi  10929  pinq  10949  mulidnq  10985  1idpr  11051  prlem934  11055  0idsr  11119  1idsr  11120  00sr  11121  negexsr  11124  recexsrlem  11125  sqgt0sr  11128  ax1rid  11183  axcnre  11186  ne0gt0  11348  peano2cn  11415  peano2re  11416  00id  11418  mul02lem2  11420  mul01  11422  subid  11510  subid1  11511  negid  11538  negeq0  11545  peano2cnm  11557  peano2rem  11558  lt0neg1  11751  le0neg1  11753  relin01  11769  div2neg  11972  recgt0ii  12156  divgt0i2i  12165  ledivp1i  12175  ltdivp1i  12176  peano5nni  12251  peano2nn  12260  nnge1  12276  nnne0  12282  times2  12385  addltmul  12485  nn0p1nn  12548  peano2nn0  12549  nn0lele2xi  12565  fcdmnn0supp  12566  fcdmnn0fsupp  12567  fcdmnn0suppg  12568  peano2z  12641  peano2zm  12643  suprzcl  12681  zeo  12687  eluzaddi  12891  uzwo  12935  uzwo2  12936  infssuzle  12955  infssuzcl  12956  zq  12978  rpnnen1lem1  13002  rpnnen1lem3  13003  rpnnen1lem5  13005  rphalfcl  13044  zgt1rpn0n1  13058  ltpnf  13144  nltmnf  13153  pnfge  13154  nltpnft  13188  xlemnf  13191  qsqueeze  13225  xlt0neg1  13243  xle0neg1  13245  xaddpnf1  13250  xaddmnf1  13252  xaddrid  13265  xsubge0  13285  xmul01  13291  xmulneg1  13293  xmulpnf1  13298  xmulrid  13303  supxrbnd  13352  supxrgtmnf  13353  supxrre1  13354  supxrre2  13355  elioopnf  13465  elicopnf  13467  iccshftri  13509  iccshftli  13511  iccdili  13513  icccntri  13515  fzprval  13607  fz0add1fz1  13756  fzofzp1  13785  fzostep1  13804  injresinj  13809  flge0nn0  13842  flge1nn  13843  btwnzge0  13850  modfrac  13906  om2uzsuci  13971  axdc4uzlem  14006  ser1const  14081  exp0  14088  exp1  14090  expn1  14094  nn0sqcl  14112  sqval  14137  sqeq0  14142  resqcl  14146  zsqcl  14151  expubnd  14199  binom21  14240  expnbnd  14253  nn0opthlem2  14290  bcnn  14333  bcn2  14340  bcn2p1  14346  bcnm1  14348  hasheq0  14384  hashsng  14390  hashen1  14391  hashunsnggt  14415  hashin  14432  hashdif  14434  hashgt23el  14445  hashxplem  14454  hashf1lem2  14477  hash2pr  14490  hash2prde  14491  pr2pwpr  14500  hash3tr  14512  iswrd  14536  wrdval  14537  hashwrdn  14567  ccatval2  14598  ccatrid  14607  eqs1  14632  s111  14635  ccatws1len  14640  repsw0  14797  repsw1  14803  cshw0  14814  wwlktovf  14977  relexpsucnnl  15051  reim0  15139  imval2  15172  cjne0  15184  abssq  15327  max0add  15331  abs2dif  15353  rddif  15361  absrdbnd  15362  rexuz3  15369  isershft  15682  isercolllem2  15684  isercoll  15686  fsum  15738  fsumadd  15758  fsumsplitsnun  15773  bcxmas  15853  infcvgaux2i  15876  fprod  15959  risefac0  16045  fallfac0  16046  risefac1  16051  fallfac1  16052  bpoly2  16075  bpoly3  16076  bpoly4  16077  fsumcube  16078  efi4p  16155  resin4p  16156  recos4p  16157  sinbnd  16198  cosbnd  16199  rpnnen2lem8  16239  rpnnen2lem12  16243  cnso  16265  dvdsmul2  16298  dvdslelem  16328  odd2np1lem  16359  mod2eq1n2dvds  16366  divalglem0  16412  divalglem1  16413  divalglem4  16415  divalglem5  16416  divalglem8  16419  flodddiv4  16434  bits0  16447  bitsp1o  16452  bitsf1  16465  sadadd2lem2  16469  gcd1  16547  lcm0val  16613  dvdslcm  16617  lcmeq0  16619  lcmgcd  16626  lcm1  16629  lcmfunsnlem2lem2  16658  lcmfunsnlem2  16659  prm2orodd  16710  phiprm  16796  pc0  16874  pcdvdstr  16896  vdwlem2  17002  vdwlem6  17006  vdwlem8  17008  hashbc0  17025  setsval  17186  fsets  17188  setsres  17197  ressinbas  17268  ressress  17270  elrestr  17444  pwssnf1o  17514  xpsfrnel  17578  xpscf  17581  ismred2  17617  submre  17619  mreacs  17672  oppchomfval  17728  brssc  17829  isssc  17835  yonedalem4c  18292  oduleval  18304  isprs  18312  oduclatb  18521  gsumval2a  18667  smndex1n0mnd  18894  mulg1  19068  mulgnegnn  19071  isghmOLD  19203  ghmghmrn  19222  cntrnsg  19331  oppgplusfval  19335  pgrpsubgsymg  19395  psgneldm2i  19491  efgrelexlemb  19736  frgp0  19746  frgpmhm  19751  vrgpf  19754  cntrcmnd  19828  cntrabl  19829  cygctb  19878  dprd0  20019  dprd2da  20030  mgpplusg  20109  opprmulfval  20304  subrngint  20528  subrgint  20563  lsp0  20975  rlmval2  21161  cncrng  21363  cnfld1  21368  zringcyg  21442  mulgrhm2  21451  zlmsca  21493  fermltlchr  21502  chrnzr  21503  zrhpsgnelbas  21566  ocvz  21650  cssincl  21660  css0  21661  css1  21662  frlmip  21752  fczpsrbag  21895  ply1idvr1OLD  22247  evls1rhmlem  22273  evl1fval1lem  22282  marrepeval  22517  decpmatid  22724  0opn  22858  topopn  22860  basdif0  22907  tgval  22909  isopn2  22986  0cld  22992  ntropn  23003  ntrval2  23005  ntrdif  23006  clsdif  23007  cmclsopn  23016  ntrtop  23024  ntr0  23035  mretopd  23046  neips  23067  neiptopnei  23086  maxlp  23101  isperf2  23106  rest0  23123  iocpnfordt  23169  icomnfordt  23170  mnfnei  23175  refref  23467  unisngl  23481  1stckgen  23508  ptbasfi  23535  pthaus  23592  fbssfi  23791  isfil2  23810  ssfg  23826  filconn  23837  fbasrn  23838  filufint  23874  imaelfm  23905  fmfnfmlem4  23911  fclsfnflim  23981  alexsubALTlem3  24003  alexsubALTlem4  24004  ustfilxp  24167  ustuqtop2  24197  ustuqtop4  24199  utopsnneiplem  24202  utopsnnei  24204  utop2nei  24205  cfiluweak  24249  neipcfilu  24250  xmetres  24319  metres  24320  mopnex  24476  prdsms  24488  metucn  24528  tngds  24605  tngngp3  24613  nmoge0  24678  cnfldnm  24735  tgioo  24753  xrtgioo  24764  xrsmopn  24770  negcncf  24884  negcncfOLD  24885  phtpy01  24953  pco0  24983  tcphtopn  25196  tchnmfval  25198  caussi  25267  rrxip  25360  minveclem3b  25398  ovolfioo  25438  ovolficc  25439  ovolfsf  25442  ovolctb  25461  ovolctb2  25463  ovolfiniun  25472  ovoliun2  25477  ovolshftlem1  25480  ovolscalem1  25484  ovolicopnf  25495  iunmbl2  25528  uniioombllem2  25554  opnmblALT  25574  ismbf  25599  mbfinf  25636  0plef  25643  itg1climres  25685  itg2cnlem1  25732  iblitg  25739  ibl0  25758  itgcn  25816  cnlimc  25859  dvfre  25925  dvnfre  25926  dveflem  25953  dvef  25954  dvlipcn  25969  lhop2  25990  itgsubstlem  26025  deg1val  26071  ply1rem  26141  coefv0  26223  plyrecj  26257  vieta1lem2  26289  aannenlem1  26306  aaliou2b  26319  ulmval  26359  ulmpm  26362  ulmdvlem1  26379  mtest  26383  efcn  26423  sin2pim  26463  cos2pim  26464  sinmpi  26465  cosmpi  26466  sinppi  26467  cosppi  26468  efimpi  26469  sincosq1lem  26475  sincosq2sgn  26477  sincosq3sgn  26478  sincosq4sgn  26479  sinq12gt0  26485  sinq34lt0t  26487  sincosq1eq  26490  abssinper  26499  efif1o  26524  loglt1b  26612  relogcn  26616  ellogdm  26617  efopn  26636  cxp0  26648  cxp1  26649  cxpsqrt  26681  logsqrt  26682  logb1  26748  atandm3  26857  atanbnd  26905  atancn  26915  leibpi  26921  efrlim  26948  efrlimOLD  26949  logdifbnd  26973  vmaprm  27096  ppip1le  27140  ppieq0  27155  prmorcht  27157  ppiublem1  27182  ppiub  27184  chpeq0  27188  chtub  27192  fsumvma  27193  pclogsum  27195  chpval2  27198  dchrresb  27239  dchrptlem1  27244  lgs0  27290  lgs2  27294  lgsdir2lem2  27306  lgsdir2lem4  27308  lgsdchrval  27334  lgsdchr  27335  lgseisenlem2  27356  2lgslem1c  27373  2lgsoddprmlem2  27389  addsq2nreurex  27424  dirith2  27508  selberg2lem  27530  qabvle  27605  qabvexp  27606  ostth  27619  noextendseq  27648  noetasuplem4  27717  noetainflem4  27721  scutun12  27791  madebdayim  27862  addsrid  27933  addsfo  27952  peano2no  27953  negscl  28004  subsfo  28031  subsid1  28034  muls01  28074  mulsrid  28075  divs1  28165  recsex  28179  abssnid  28203  peano2ons  28224  noseqp1  28233  noseqind  28234  peano2nns  28289  dfnns2  28298  elzs2  28321  elnnzs  28323  elznns  28324  n0seo  28341  exps0  28346  exps1  28347  istrkg2ld  28404  istrkg3ld  28405  ttgval  28819  ttgvalOLD  28820  brbtwn  28844  colinearalglem4  28854  upgr0eop  29059  uspgrushgr  29122  usgruspgr  29125  usgr0eop  29191  0grsubgr  29223  uspgrloopvtx  29461  umgr2v2evtx  29467  usgr0edg0rusgr  29521  rgrusgrprc  29535  wlkvtxiedg  29571  pthdivtx  29675  usgr2pthlem  29711  wlkswwlksf1o  29827  wwlksext2clwwlk  30004  konigsbergssiedgw  30197  frgrncvvdeqlem7  30252  2clwwlk2  30295  ex-po  30382  pliguhgr  30433  nvnd  30635  ipval2lem3  30652  ipval2  30654  ipidsq  30657  dipcj  30661  dip0r  30664  nmlnogt0  30744  blocni  30752  ipasslem2  30779  ipasslem8  30784  ipasslem9  30785  ajval  30808  ubthlem1  30817  hvaddlid  30970  hvsub0  31023  hi02  31044  hlimi  31135  isch2  31170  chlimi  31181  chsupunss  31291  shsupunss  31293  chlejb1i  31423  h1dei  31497  h1de2ci  31503  spanunsni  31526  pjoml2i  31532  pjorthi  31616  mayete3i  31675  hosubid1  31745  nmopge0  31858  nmfnge0  31874  adj1  31880  adjeq  31882  lnop0  31913  lnopmi  31947  nmophmi  31978  cnlnadjlem5  32018  cnlnadjeui  32024  unierri  32051  leoprf2  32074  leopnmid  32085  nmopleid  32086  hstles  32178  hst0  32180  strlem3a  32199  dmdbr2  32250  mdsl1i  32268  mdsl2i  32269  mdsl2bi  32270  cvmdi  32271  mdslmd1lem1  32272  mdslmd1lem2  32273  mdslmd1i  32276  mdslmd2i  32277  csmdsymi  32281  mdexchi  32282  superpos  32301  atomli  32329  atordi  32331  chirredlem1  32337  chirredlem2  32338  atcvat4i  32344  atabsi  32348  mdsymlem1  32350  mdsymlem5  32354  mdsymlem6  32355  sumdmdii  32362  dmdbr5ati  32369  dmdbr6ati  32370  mddmdin0i  32378  cdj3lem2  32382  unidifsnel  32483  unidifsnne  32484  xppreima  32590  abfmpunirn  32597  abfmpel  32600  aciunf1lem  32607  fgreu  32617  imafi2  32658  padct  32666  fpwrelmapffslem  32678  fpwrelmap  32679  xrge0infss  32701  xrdifh  32721  pfx1s2  32863  clatp0cl  32905  clatp1cl  32906  cntrcrng  33012  cycpmco2lem4  33088  rmfsupp2  33181  1fldgenq  33264  resvval  33293  rearchi  33309  qusxpid  33326  opprabs  33445  zringfrac  33517  rlmdim  33595  constrfiss  33731  2sqr3minply  33749  locfinreflem  33798  locfinref  33799  ordtconnlem1  33882  rge0scvg  33907  lmxrge0  33910  qqh0  33944  qqh1  33945  rrh0  33975  zrhre  33979  esumcst  34023  esumfzf  34029  esumfsupre  34031  hasheuni  34045  sgon  34084  dmvlsiga  34089  sigainb  34096  measval  34158  ismeas  34159  sxbrsigalem0  34232  omssubadd  34261  carsggect  34279  eulerpartlemmf  34336  eulerpartlemgs2  34341  eulerpartlemn  34342  rrvsum  34415  ballotlem2  34450  ballotlemfcc  34455  ballotlem4  34460  signsplypnf  34524  signsply0  34525  signsw0glem  34527  signswrid  34532  signlem0  34561  signshf  34562  bnj535  34863  bnj580  34886  bnj907  34940  bnj1253  34990  funen1cnv  35061  loop1cycl  35101  ptpconn  35197  cvmsss2  35238  cvmlift2lem12  35278  cvmlift2lem13  35279  cvmliftphtlem  35281  cvmliftpht  35282  fmlafvel  35349  mppsthm  35543  bcneg1  35695  fv1stcnv  35736  fv2ndcnv  35737  wlimeq1  35780  imagesset  35913  altopeq1  35923  brcolinear2  36018  cldbnd  36286  ivthALT  36295  refssfne  36318  ontgval  36391  onint1  36409  axc11n11r  36643  bj-pm11.53a  36738  bj-bm1.3ii  37024  bj-restsn0  37045  bj-restsn10  37046  bj-restsnid  37047  bj-rest10  37048  bj-rest0  37053  bj-inftyexpiinv  37168  bj-inftyexpidisj  37170  taupilem1  37281  irrdiff  37286  f1omptsnlem  37296  mptsnunlem  37298  topdifinffinlem  37307  inunissunidif  37335  rdgssun  37338  exrecfnlem  37339  exrecfnpw  37341  finixpnum  37571  tan2h  37578  matunitlindflem2  37583  ptrest  37585  poimirlem22  37608  poimirlem25  37611  mblfinlem1  37623  mblfinlem2  37624  mblfinlem3  37625  mblfinlem4  37626  ismblfin  37627  itg2addnclem  37637  itg2addnclem2  37638  itg2addnclem3  37639  itg2addnc  37640  itg2gt0cn  37641  ftc1anclem5  37663  ftc1anclem8  37666  dvasin  37670  dvacos  37671  sdclem2  37708  totbndbnd  37755  heibor1lem  37775  heiborlem7  37783  bfplem1  37788  prnc  38033  ecexALTV  38291  brxrn  38334  riotasv  38919  glbconN  39337  glbconNOLD  39338  atpointN  39704  polsubN  39868  pol0N  39870  pol1N  39871  2polvalN  39875  2polssN  39876  3polN  39877  pcl0N  39883  2pmaplubN  39887  pnonsingN  39894  polsubclN  39913  cdlemefs32sn1aw  40375  cdleme43fsv1snlem  40381  cdleme41sn3a  40394  cdleme32a  40402  cdleme40m  40428  cdleme40n  40429  cdleme42b  40439  istendo  40721  cdlemk40  40878  cdlemkid  40897  dihvalcqpre  41196  facp2  42103  fac2xp3  42199  2xp3dxp2ge1d  42201  factwoffsmonot  42202  relt0neg1  42437  sn-nnne0  42441  sn-inelr  42460  frlmsnic  42513  prjspnerlem  42590  prjspnval2  42591  0prjspn  42601  3cubes  42664  mapfzcons1cl  42692  eldioph3b  42739  eldiophss  42748  0dioph  42752  vdioph  42753  eldioph4b  42785  eldioph4i  42786  rencldnfilem  42794  rmxy1  42897  rmxy0  42898  rmxm1  42909  rmym1  42910  monotoddzzfi  42917  wepwso  43018  aomclem6  43034  pwslnmlem0  43066  isnumbasabl  43081  areaquad  43191  onexlimgt  43218  oaabsb  43269  nadd1suc  43367  om2  43379  oe2  43381  safesnsupfidom1o  43392  onno  43408  oa1cl  43422  finona1cl  43428  reabsifneg  43607  reabsifnneg  43610  relexp2  43652  eltrclrec  43655  elrtrclrec  43656  brtrclrec  43671  brrtrclrec  43672  relexpxpmin  43692  dftrcl3  43695  dfrtrcl3  43708  heeq1  43752  seff  44285  lhe4.4ex1a  44305  eelT0  44752  snssl  44807  sineq0ALT  44914  trfr  44936  xpwf  44938  dmwf  44939  rnwf  44940  modelaxreplem1  44952  modelaxreplem3  44954  0elaxnul  44957  prclaxpr  44959  uniclaxun  44960  wfac8prim  44976  elrnmpt1sf  45151  founiiun0  45152  supxrgere  45301  supxrgelem  45305  fmuldfeqlem1  45554  fmuldfeq  45555  climneg  45582  sumnnodd  45602  liminfltlem  45776  xlimpnfxnegmnf2  45830  addccncf2  45848  dvsinax  45885  stoweidlem18  45990  stoweidlem19  45991  stoweidlem22  45994  stoweidlem34  46006  stoweidlem40  46012  stoweidlem41  46013  stoweidlem55  46027  stoweidlem59  46031  dirker2re  46064  dirkerdenne0  46065  fourierdlem48  46126  fourierdlem49  46127  fourierdlem70  46148  fourierdlem71  46149  fourierdlem104  46182  fourierdlem112  46190  fouriersw  46203  etransclem46  46252  etransclem48  46254  nnfoctbdjlem  46427  ormklocald  46846  natlocalincr  46848  singoutnword  46854  sqrtnegnre  47277  fsummmodsnunz  47320  flsqrt5  47539  bits0ALTV  47624  mogoldbblem  47665  sgoldbeven3prm  47728  nnsum3primes4  47733  isubgr0uhgr  47817  ushggricedg  47854  2zrngnmlid  48129  2zrngnmrid  48130  mpoexxg2  48212  lco0  48302  zlmodzxzldeplem3  48377  0dig1  48488  naryfvalel  48509  ackvalsuc0val  48566  0funclem  48888  aacllem  49328