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 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  704  mp3an23  1453  elvd  3494  eueq2  3732  sbcgf  3881  sbcralg  3896  csbconstgf  3939  sbcnestgw  4446  csbnestgw  4447  sbcnestg  4451  csbnestg  4452  csbnest1g  4455  mpteq1OLD  5260  iinexg  5366  eusv2nf  5413  reusv2lem5  5420  nnullss  5482  xpss1  5719  xpiindi  5860  reldm0  5952  elrnmpt1s  5982  resdm  6055  eliniseg  6124  trinxp  6157  ssrnres  6209  cnveq0  6228  coi2  6294  relrelss  6304  cnviin  6317  elpred  6349  onelssex  6443  ord0eln0  6450  funcnvres  6656  funimaex  6666  fnresin1  6705  fnresin2  6706  fresin  6790  ssimaex  7007  fvmpt  7029  fvmptnf  7051  fvimacnvALT  7090  dff3  7134  fsn  7169  fsn2  7170  funop  7183  fvrnressn  7195  fninfp  7208  fndifnfp  7210  fnnfpeq0  7212  fprb  7231  elabrex  7279  elabrexg  7280  f1elima  7300  f1ofvswap  7342  fliftel1  7346  f1owe  7389  sorpssuni  7767  sorpssint  7768  eldifpw  7803  ordeleqon  7817  ordsson  7818  ssnlim  7923  abrexexg  8001  tposfun  8283  tpostpos2  8288  fpr3g  8326  wfr3g  8363  wfrlem14OLD  8378  wfrlem15OLD  8379  tfrlem10  8443  tfrlem12  8445  tfr3  8455  seqomlem1  8506  seqomlem2  8507  seqomlem4  8509  ondif2  8558  oa0  8572  om0  8573  oa1suc  8587  om1  8598  oe1  8600  oe1m  8601  omass  8636  oeoalem  8652  oeoelem  8654  nnmsucr  8681  nnm1  8708  nnm2  8709  naddrid  8739  naddlid  8740  ecelqsg  8830  xpider  8846  mapdm0  8900  fvdiagfn  8949  ixpsnf1o  8996  xp1en  9123  undom  9125  sbthlem7  9155  domunsn  9193  xpmapenlem  9210  infensuc  9221  findcard2d  9232  diffi  9242  cnvfi  9243  enreffi  9249  snnen2o  9300  1sdom2dom  9310  infi  9330  finresfin  9332  unblem1  9356  unblem2  9357  unblem3  9358  unblem4  9359  isfinite2  9362  infn0ALT  9369  unfilem1  9371  unfilem2  9372  unfir  9374  fofinf1o  9400  cnvfiALT  9407  pwfilemOLD  9416  mptfi  9421  finsschain  9429  marypha2  9508  inf0  9690  trcl  9797  frr3g  9825  r1rankidb  9873  snwf  9878  unwf  9879  uniwf  9888  rankval3b  9895  rankr1a  9905  rankxplim3  9950  scott0  9955  djueq1  9974  card1  10037  pm54.43  10070  infxpenc2  10091  dfac8clem  10101  alephsuc2  10149  alephle  10157  cardaleph  10158  dfac12lem2  10214  undjudom  10237  djudom1  10252  pwdju1  10260  nnadju  10267  ackbij1lem18  10305  cflem  10314  cflemOLD  10315  cflecard  10322  cfeq0  10325  cfslb  10335  cfsmolem  10339  cfcoflem  10341  cfidm  10344  isfin4p1  10384  fin23lem12  10400  fin23lem16  10404  fin23lem28  10409  fin23lem38  10418  fin23lem41  10421  fin1a2lem7  10475  fin1a2lem12  10480  fin1a2lem13  10481  hsmexlem8  10493  axcc2lem  10505  axcc3  10507  domtriomlem  10511  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  ac6num  10548  ttukeylem4  10581  ttukeylem7  10584  ttukey2g  10585  axdclem  10588  brdom3  10597  brdom5  10598  cardeq0  10621  unsnen  10622  konigthlem  10637  pwcfsdom  10652  canthp1lem1  10721  wunex2  10807  wuncval2  10816  eltsk2g  10820  ingru  10884  grutsk  10891  axgroth6  10897  mulidpi  10955  nlt1pi  10975  indpi  10976  pinq  10996  mulidnq  11032  1idpr  11098  prlem934  11102  0idsr  11166  1idsr  11167  00sr  11168  negexsr  11171  recexsrlem  11172  sqgt0sr  11175  ax1rid  11230  axcnre  11233  ne0gt0  11395  peano2cn  11462  peano2re  11463  00id  11465  mul02lem2  11467  mul01  11469  subid  11555  subid1  11556  negid  11583  negeq0  11590  peano2cnm  11602  peano2rem  11603  lt0neg1  11796  le0neg1  11798  relin01  11814  div2neg  12017  recgt0ii  12201  divgt0i2i  12210  ledivp1i  12220  ltdivp1i  12221  peano5nni  12296  peano2nn  12305  nnge1  12321  nnne0  12327  times2  12430  addltmul  12529  nn0p1nn  12592  peano2nn0  12593  nn0lele2xi  12608  fcdmnn0supp  12609  fcdmnn0fsupp  12610  fcdmnn0suppg  12611  peano2z  12684  peano2zm  12686  suprzcl  12723  zeo  12729  eluzaddi  12934  uzwo  12976  uzwo2  12977  infssuzle  12996  infssuzcl  12997  zq  13019  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  rphalfcl  13084  zgt1rpn0n1  13098  ltpnf  13183  nltmnf  13192  pnfge  13193  nltpnft  13226  xlemnf  13229  qsqueeze  13263  xlt0neg1  13281  xle0neg1  13283  xaddpnf1  13288  xaddmnf1  13290  xaddrid  13303  xsubge0  13323  xmul01  13329  xmulneg1  13331  xmulpnf1  13336  xmulrid  13341  supxrbnd  13390  supxrgtmnf  13391  supxrre1  13392  supxrre2  13393  elioopnf  13503  elicopnf  13505  iccshftri  13547  iccshftli  13549  iccdili  13551  icccntri  13553  fzprval  13645  fz0add1fz1  13786  fzofzp1  13814  fzostep1  13833  injresinj  13838  flge0nn0  13871  flge1nn  13872  btwnzge0  13879  modfrac  13935  om2uzsuci  13999  axdc4uzlem  14034  ser1const  14109  exp0  14116  exp1  14118  expn1  14122  nn0sqcl  14140  sqval  14165  sqeq0  14170  resqcl  14174  zsqcl  14179  expubnd  14227  binom21  14268  expnbnd  14281  nn0opthlem2  14318  bcnn  14361  bcn2  14368  bcn2p1  14374  bcnm1  14376  hasheq0  14412  hashsng  14418  hashen1  14419  hashunsnggt  14443  hashin  14460  hashdif  14462  hashgt23el  14473  hashxplem  14482  hashf1lem2  14505  hash2pr  14518  hash2prde  14519  pr2pwpr  14528  hash3tr  14540  iswrd  14564  wrdval  14565  hashwrdn  14595  ccatval2  14626  ccatrid  14635  eqs1  14660  s111  14663  ccatws1len  14668  repsw0  14825  repsw1  14831  cshw0  14842  wwlktovf  15005  relexpsucnnl  15079  reim0  15167  imval2  15200  cjne0  15212  abssq  15355  max0add  15359  abs2dif  15381  rddif  15389  absrdbnd  15390  rexuz3  15397  isershft  15712  isercolllem2  15714  isercoll  15716  fsum  15768  fsumadd  15788  fsumsplitsnun  15803  bcxmas  15883  infcvgaux2i  15906  fprod  15989  risefac0  16075  fallfac0  16076  risefac1  16081  fallfac1  16082  bpoly2  16105  bpoly3  16106  bpoly4  16107  fsumcube  16108  efi4p  16185  resin4p  16186  recos4p  16187  sinbnd  16228  cosbnd  16229  rpnnen2lem8  16269  rpnnen2lem12  16273  cnso  16295  dvdsmul2  16327  dvdslelem  16357  odd2np1lem  16388  mod2eq1n2dvds  16395  divalglem0  16441  divalglem1  16442  divalglem4  16444  divalglem5  16445  divalglem8  16448  flodddiv4  16461  bits0  16474  bitsp1o  16479  bitsf1  16492  sadadd2lem2  16496  gcd1  16574  lcm0val  16641  dvdslcm  16645  lcmeq0  16647  lcmgcd  16654  lcm1  16657  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  prm2orodd  16738  phiprm  16824  pc0  16901  pcdvdstr  16923  vdwlem2  17029  vdwlem6  17033  vdwlem8  17035  hashbc0  17052  setsval  17214  fsets  17216  setsres  17225  ressinbas  17304  ressress  17307  elrestr  17488  pwssnf1o  17558  xpsfrnel  17622  xpscf  17625  ismred2  17661  submre  17663  mreacs  17716  oppchomfval  17772  oppchomfvalOLD  17773  brssc  17875  isssc  17881  yonedalem4c  18347  oduleval  18359  isprs  18367  oduclatb  18577  gsumval2a  18723  smndex1n0mnd  18947  mulg1  19121  mulgnegnn  19124  isghmOLD  19256  ghmghmrn  19275  cntrnsg  19384  oppgplusfval  19388  pgrpsubgsymg  19451  psgneldm2i  19547  efgrelexlemb  19792  frgp0  19802  frgpmhm  19807  vrgpf  19810  cntrcmnd  19884  cntrabl  19885  cygctb  19934  dprd0  20075  dprd2da  20086  mgpplusg  20165  opprmulfval  20362  subrngint  20586  subrgint  20623  lsp0  21030  sralemOLD  21199  rlmval2  21222  cncrng  21424  cnfld1  21429  zringcyg  21503  mulgrhm2  21512  zlmsca  21558  fermltlchr  21567  chrnzr  21568  zrhpsgnelbas  21635  ocvz  21719  cssincl  21729  css0  21730  css1  21731  frlmip  21821  fczpsrbag  21964  ply1idvr1OLD  22320  evls1rhmlem  22346  evl1fval1lem  22355  marrepeval  22590  decpmatid  22797  0opn  22931  topopn  22933  basdif0  22981  tgval  22983  isopn2  23061  0cld  23067  ntropn  23078  ntrval2  23080  ntrdif  23081  clsdif  23082  cmclsopn  23091  ntrtop  23099  ntr0  23110  mretopd  23121  neips  23142  neiptopnei  23161  maxlp  23176  isperf2  23181  rest0  23198  iocpnfordt  23244  icomnfordt  23245  mnfnei  23250  refref  23542  unisngl  23556  1stckgen  23583  ptbasfi  23610  pthaus  23667  fbssfi  23866  isfil2  23885  ssfg  23901  filconn  23912  fbasrn  23913  filufint  23949  imaelfm  23980  fmfnfmlem4  23986  fclsfnflim  24056  alexsubALTlem3  24078  alexsubALTlem4  24079  ustfilxp  24242  ustuqtop2  24272  ustuqtop4  24274  utopsnneiplem  24277  utopsnnei  24279  utop2nei  24280  cfiluweak  24325  neipcfilu  24326  xmetres  24395  metres  24396  mopnex  24553  prdsms  24565  metucn  24605  tngds  24689  tngdsOLD  24690  tngngp3  24698  nmoge0  24763  cnfldnm  24820  tgioo  24837  xrtgioo  24847  xrsmopn  24853  negcncf  24967  negcncfOLD  24968  phtpy01  25036  pco0  25066  tcphtopn  25279  tchnmfval  25281  caussi  25350  rrxip  25443  minveclem3b  25481  ovolfioo  25521  ovolficc  25522  ovolfsf  25525  ovolctb  25544  ovolctb2  25546  ovolfiniun  25555  ovoliun2  25560  ovolshftlem1  25563  ovolscalem1  25567  ovolicopnf  25578  iunmbl2  25611  uniioombllem2  25637  opnmblALT  25657  ismbf  25682  mbfinf  25719  0plef  25726  itg1climres  25769  itg2cnlem1  25816  iblitg  25823  ibl0  25842  itgcn  25900  cnlimc  25943  dvfre  26009  dvnfre  26010  dveflem  26037  dvef  26038  dvlipcn  26053  lhop2  26074  itgsubstlem  26109  deg1val  26155  ply1rem  26225  coefv0  26307  plyrecj  26339  vieta1lem2  26371  aannenlem1  26388  aaliou2b  26401  ulmval  26441  ulmpm  26444  ulmdvlem1  26461  mtest  26465  efcn  26505  sin2pim  26545  cos2pim  26546  sinmpi  26547  cosmpi  26548  sinppi  26549  cosppi  26550  efimpi  26551  sincosq1lem  26557  sincosq2sgn  26559  sincosq3sgn  26560  sincosq4sgn  26561  sinq12gt0  26567  sinq34lt0t  26569  sincosq1eq  26572  abssinper  26581  efif1o  26606  loglt1b  26694  relogcn  26698  ellogdm  26699  efopn  26718  cxp0  26730  cxp1  26731  cxpsqrt  26763  logsqrt  26764  logb1  26830  atandm3  26939  atanbnd  26987  atancn  26997  leibpi  27003  efrlim  27030  efrlimOLD  27031  logdifbnd  27055  vmaprm  27178  ppip1le  27222  ppieq0  27237  prmorcht  27239  ppiublem1  27264  ppiub  27266  chpeq0  27270  chtub  27274  fsumvma  27275  pclogsum  27277  chpval2  27280  dchrresb  27321  dchrptlem1  27326  lgs0  27372  lgs2  27376  lgsdir2lem2  27388  lgsdir2lem4  27390  lgsdchrval  27416  lgsdchr  27417  lgseisenlem2  27438  2lgslem1c  27455  2lgsoddprmlem2  27471  addsq2nreurex  27506  dirith2  27590  selberg2lem  27612  qabvle  27687  qabvexp  27688  ostth  27701  noextendseq  27730  noetasuplem4  27799  noetainflem4  27803  scutun12  27873  madebdayim  27944  addsrid  28015  addsfo  28034  peano2no  28035  negscl  28086  subsfo  28113  subsid1  28116  muls01  28156  mulsrid  28157  divs1  28247  recsex  28261  abssnid  28285  peano2ons  28306  noseqp1  28315  noseqind  28316  peano2nns  28371  dfnns2  28380  elzs2  28403  elnnzs  28405  elznns  28406  n0seo  28423  exps0  28428  exps1  28429  istrkg2ld  28486  istrkg3ld  28487  ttgval  28901  ttgvalOLD  28902  cchhllemOLD  28920  brbtwn  28932  colinearalglem4  28942  upgr0eop  29149  uspgrushgr  29212  usgruspgr  29215  usgr0eop  29281  0grsubgr  29313  uspgrloopvtx  29551  umgr2v2evtx  29557  usgr0edg0rusgr  29611  rgrusgrprc  29625  wlkvtxiedg  29661  pthdivtx  29765  usgr2pthlem  29799  wlkswwlksf1o  29912  wwlksext2clwwlk  30089  konigsbergssiedgw  30282  frgrncvvdeqlem7  30337  2clwwlk2  30380  ex-po  30467  pliguhgr  30518  nvnd  30720  ipval2lem3  30737  ipval2  30739  ipidsq  30742  dipcj  30746  dip0r  30749  nmlnogt0  30829  blocni  30837  ipasslem2  30864  ipasslem8  30869  ipasslem9  30870  ajval  30893  ubthlem1  30902  hvaddlid  31055  hvsub0  31108  hi02  31129  hlimi  31220  isch2  31255  chlimi  31266  chsupunss  31376  shsupunss  31378  chlejb1i  31508  h1dei  31582  h1de2ci  31588  spanunsni  31611  pjoml2i  31617  pjorthi  31701  mayete3i  31760  hosubid1  31830  nmopge0  31943  nmfnge0  31959  adj1  31965  adjeq  31967  lnop0  31998  lnopmi  32032  nmophmi  32063  cnlnadjlem5  32103  cnlnadjeui  32109  unierri  32136  leoprf2  32159  leopnmid  32170  nmopleid  32171  hstles  32263  hst0  32265  strlem3a  32284  dmdbr2  32335  mdsl1i  32353  mdsl2i  32354  mdsl2bi  32355  cvmdi  32356  mdslmd1lem1  32357  mdslmd1lem2  32358  mdslmd1i  32361  mdslmd2i  32362  csmdsymi  32366  mdexchi  32367  superpos  32386  atomli  32414  atordi  32416  chirredlem1  32422  chirredlem2  32423  atcvat4i  32429  atabsi  32433  mdsymlem1  32435  mdsymlem5  32439  mdsymlem6  32440  sumdmdii  32447  dmdbr5ati  32454  dmdbr6ati  32455  mddmdin0i  32463  cdj3lem2  32467  unidifsnel  32563  unidifsnne  32564  xppreima  32664  abfmpunirn  32670  abfmpel  32673  aciunf1lem  32680  fgreu  32690  imafi2  32725  padct  32733  fpwrelmapffslem  32746  fpwrelmap  32747  xrge0infss  32767  xrdifh  32785  pfx1s2  32905  clatp0cl  32949  clatp1cl  32950  cntrcrng  33046  cycpmco2lem4  33122  rmfsupp2  33218  1fldgenq  33289  resvval  33318  rearchi  33339  qusxpid  33356  opprabs  33475  zringfrac  33547  rlmdim  33622  2sqr3minply  33738  locfinreflem  33786  locfinref  33787  ordtconnlem1  33870  rge0scvg  33895  lmxrge0  33898  qqh0  33930  qqh1  33931  rrh0  33961  zrhre  33965  esumcst  34027  esumfzf  34033  esumfsupre  34035  hasheuni  34049  sgon  34088  dmvlsiga  34093  sigainb  34100  measval  34162  ismeas  34163  sxbrsigalem0  34236  omssubadd  34265  carsggect  34283  eulerpartlemmf  34340  eulerpartlemgs2  34345  eulerpartlemn  34346  rrvsum  34419  ballotlem2  34453  ballotlemfcc  34458  ballotlem4  34463  signsplypnf  34527  signsply0  34528  signsw0glem  34530  signswrid  34535  signlem0  34564  signshf  34565  bnj535  34866  bnj580  34889  bnj907  34943  bnj1253  34993  funen1cnv  35064  loop1cycl  35105  ptpconn  35201  cvmsss2  35242  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmliftphtlem  35285  cvmliftpht  35286  fmlafvel  35353  mppsthm  35547  bcneg1  35698  fv1stcnv  35740  fv2ndcnv  35741  wlimeq1  35784  imagesset  35917  altopeq1  35927  brcolinear2  36022  cldbnd  36292  ivthALT  36301  refssfne  36324  ontgval  36397  onint1  36415  axc11n11r  36649  bj-pm11.53a  36744  bj-bm1.3ii  37030  bj-restsn0  37051  bj-restsn10  37052  bj-restsnid  37053  bj-rest10  37054  bj-rest0  37059  bj-inftyexpiinv  37174  bj-inftyexpidisj  37176  taupilem1  37287  irrdiff  37292  f1omptsnlem  37302  mptsnunlem  37304  topdifinffinlem  37313  inunissunidif  37341  rdgssun  37344  exrecfnlem  37345  exrecfnpw  37347  finixpnum  37565  tan2h  37572  matunitlindflem2  37577  ptrest  37579  poimirlem22  37602  poimirlem25  37605  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnclem2  37632  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  ftc1anclem5  37657  ftc1anclem8  37660  dvasin  37664  dvacos  37665  sdclem2  37702  totbndbnd  37749  heibor1lem  37769  heiborlem7  37777  bfplem1  37782  prnc  38027  ecexALTV  38287  brxrn  38330  riotasv  38915  glbconN  39333  glbconNOLD  39334  atpointN  39700  polsubN  39864  pol0N  39866  pol1N  39867  2polvalN  39871  2polssN  39872  3polN  39873  pcl0N  39879  2pmaplubN  39883  pnonsingN  39890  polsubclN  39909  cdlemefs32sn1aw  40371  cdleme43fsv1snlem  40377  cdleme41sn3a  40390  cdleme32a  40398  cdleme40m  40424  cdleme40n  40425  cdleme42b  40435  istendo  40717  cdlemk40  40874  cdlemkid  40893  dihvalcqpre  41192  facp2  42100  fac2xp3  42196  2xp3dxp2ge1d  42198  factwoffsmonot  42199  fnsnbt  42225  relt0neg1  42420  sn-nnne0  42424  sn-inelr  42443  frlmsnic  42495  prjspnerlem  42572  prjspnval2  42573  0prjspn  42583  3cubes  42646  mapfzcons1cl  42674  eldioph3b  42721  eldiophss  42730  0dioph  42734  vdioph  42735  eldioph4b  42767  eldioph4i  42768  rencldnfilem  42776  rmxy1  42879  rmxy0  42880  rmxm1  42891  rmym1  42892  monotoddzzfi  42899  wepwso  43000  aomclem6  43016  pwslnmlem0  43048  isnumbasabl  43063  areaquad  43177  onexlimgt  43204  oaabsb  43256  nadd1suc  43354  om2  43366  oe2  43368  safesnsupfidom1o  43379  onno  43395  oa1cl  43409  finona1cl  43415  reabsifneg  43594  reabsifnneg  43597  relexp2  43639  eltrclrec  43642  elrtrclrec  43643  brtrclrec  43658  brrtrclrec  43659  relexpxpmin  43679  dftrcl3  43682  dfrtrcl3  43695  heeq1  43739  seff  44278  lhe4.4ex1a  44298  eelT0  44746  snssl  44801  sineq0ALT  44908  xpwf  44912  dmwf  44913  rnwf  44914  elrnmpt1sf  45096  founiiun0  45097  supxrgere  45248  supxrgelem  45252  fmuldfeqlem1  45503  fmuldfeq  45504  climneg  45531  sumnnodd  45551  liminfltlem  45725  xlimpnfxnegmnf2  45779  addccncf2  45797  dvsinax  45834  stoweidlem18  45939  stoweidlem19  45940  stoweidlem22  45943  stoweidlem34  45955  stoweidlem40  45961  stoweidlem41  45962  stoweidlem55  45976  stoweidlem59  45980  dirker2re  46013  dirkerdenne0  46014  fourierdlem48  46075  fourierdlem49  46076  fourierdlem70  46097  fourierdlem71  46098  fourierdlem104  46131  fourierdlem112  46139  fouriersw  46152  etransclem46  46201  etransclem48  46203  nnfoctbdjlem  46376  natlocalincr  46795  singoutnword  46801  upwrdfi  46806  sqrtnegnre  47222  fsummmodsnunz  47249  flsqrt5  47468  bits0ALTV  47553  mogoldbblem  47594  sgoldbeven3prm  47657  nnsum3primes4  47662  isubgr0uhgr  47743  ushggricedg  47780  2zrngnmlid  47978  2zrngnmrid  47979  mpoexxg2  48062  lco0  48156  zlmodzxzldeplem3  48231  0dig1  48343  naryfvalel  48364  ackvalsuc0val  48421  aacllem  48895