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  3443  elabg  3628  eueq2  3665  sbcgf  3808  sbcralg  3821  csbconstgf  3864  sbcnestgw  4372  csbnestgw  4373  sbcnestg  4377  csbnestg  4378  csbnest1g  4381  iinexg  5290  eusv2nf  5337  reusv2lem5  5344  nnullss  5407  xpss1  5640  xpiindi  5781  reldm0  5874  elrnmpt1s  5905  resdm  5982  eliniseg  6050  trinxp  6079  ssrnres  6133  cnveq0  6152  coi2  6219  relrelss  6228  cnviin  6241  elpred  6273  onelssex  6363  ord0eln0  6370  funcnvres  6567  funimaex  6577  fnresin1  6614  fnresin2  6615  fresin  6700  ssimaex  6916  fvmpt  6938  fvmptnf  6960  fvimacnvALT  6999  dff3  7042  fsn  7077  fsn2  7078  funop  7091  fvrnressn  7103  fnsnbg  7107  fninfp  7117  fndifnfp  7119  fnnfpeq0  7121  fprb  7137  elabrex  7185  elabrexg  7186  f1elima  7206  f1ofvswap  7249  fliftel1  7253  f1owe  7296  sorpssuni  7674  sorpssint  7675  eldifpw  7710  ordeleqon  7724  ordsson  7725  ssnlim  7825  abrexexg  7902  tposfun  8181  tpostpos2  8186  fpr3g  8224  wfr3g  8258  tfrlem10  8315  tfrlem12  8317  tfr3  8327  seqomlem1  8378  seqomlem2  8379  seqomlem4  8381  ondif2  8426  oa0  8440  om0  8441  oa1suc  8455  om1  8466  oe1  8468  oe1m  8469  omass  8504  oeoalem  8520  oeoelem  8522  nnmsucr  8549  nnm1  8576  nnm2  8577  naddrid  8607  naddlid  8608  ecelqs  8701  xpider  8721  mapdm0  8775  fvdiagfn  8825  ixpsnf1o  8872  xp1en  8987  undom  8989  sbthlem7  9017  domunsn  9051  xpmapenlem  9068  infensuc  9079  findcard2d  9087  diffi  9095  cnvfi  9096  enreffi  9103  snnen2o  9140  1sdom2dom  9149  infi  9165  finresfin  9167  unblem1  9187  unblem2  9188  unblem3  9189  unblem4  9190  isfinite2  9193  infn0ALT  9198  unfilem1  9200  unfilem2  9201  unfir  9203  fofinf1o  9227  cnvfiALT  9234  mptfi  9246  finsschain  9254  marypha2  9334  inf0  9522  trcl  9629  frr3g  9660  r1rankidb  9708  snwf  9713  unwf  9714  uniwf  9723  rankval3b  9730  rankr1a  9740  rankxplim3  9785  scott0  9790  djueq1  9809  card1  9872  pm54.43  9905  infxpenc2  9924  dfac8clem  9934  alephsuc2  9982  alephle  9990  cardaleph  9991  dfac12lem2  10047  undjudom  10070  djudom1  10085  pwdju1  10093  nnadju  10100  ackbij1lem18  10138  cflem  10147  cflemOLD  10148  cflecard  10155  cfeq0  10158  cfslb  10168  cfsmolem  10172  cfcoflem  10174  cfidm  10177  isfin4p1  10217  fin23lem12  10233  fin23lem16  10237  fin23lem28  10242  fin23lem38  10251  fin23lem41  10254  fin1a2lem7  10308  fin1a2lem12  10313  fin1a2lem13  10314  hsmexlem8  10326  axcc2lem  10338  axcc3  10340  domtriomlem  10344  axdc3lem2  10353  axdc3lem4  10355  axdc4lem  10357  axcclem  10359  ac6num  10381  ttukeylem4  10414  ttukeylem7  10417  ttukey2g  10418  axdclem  10421  brdom3  10430  brdom5  10431  cardeq0  10454  unsnen  10455  konigthlem  10470  pwcfsdom  10485  canthp1lem1  10554  wunex2  10640  wuncval2  10649  eltsk2g  10653  ingru  10717  grutsk  10724  axgroth6  10730  mulidpi  10788  nlt1pi  10808  indpi  10809  pinq  10829  mulidnq  10865  1idpr  10931  prlem934  10935  0idsr  10999  1idsr  11000  00sr  11001  negexsr  11004  recexsrlem  11005  sqgt0sr  11008  ax1rid  11063  axcnre  11066  ne0gt0  11229  peano2cn  11296  peano2re  11297  00id  11299  mul02lem2  11301  mul01  11303  subid  11391  subid1  11392  negid  11419  negeq0  11426  peano2cnm  11438  peano2rem  11439  lt0neg1  11634  le0neg1  11636  relin01  11652  div2neg  11855  recgt0ii  12039  divgt0i2i  12048  ledivp1i  12058  ltdivp1i  12059  inelr  12126  peano5nni  12139  peano2nn  12148  nnge1  12164  nnne0  12170  times2  12268  addltmul  12368  nn0p1nn  12431  peano2nn0  12432  nn0lele2xi  12448  fcdmnn0supp  12449  fcdmnn0fsupp  12450  fcdmnn0suppg  12451  peano2z  12523  peano2zm  12525  suprzcl  12563  zeo  12569  eluzaddi  12773  uzwo  12815  uzwo2  12816  infssuzle  12835  infssuzcl  12836  zq  12858  rpnnen1lem1  12882  rpnnen1lem3  12883  rpnnen1lem5  12885  rphalfcl  12925  zgt1rpn0n1  12939  ltpnf  13025  nltmnf  13034  pnfge  13035  nltpnft  13070  xlemnf  13073  qsqueeze  13107  xlt0neg1  13125  xle0neg1  13127  xaddpnf1  13132  xaddmnf1  13134  xaddrid  13147  xsubge0  13167  xmul01  13173  xmulneg1  13175  xmulpnf1  13180  xmulrid  13185  supxrbnd  13234  supxrgtmnf  13235  supxrre1  13236  supxrre2  13237  elioopnf  13350  elicopnf  13352  iccshftri  13394  iccshftli  13396  iccdili  13398  icccntri  13400  fzprval  13492  fz0add1fz1  13642  fzofzp1  13671  fzostep1  13693  injresinj  13698  flge0nn0  13731  flge1nn  13732  btwnzge0  13739  modfrac  13795  om2uzsuci  13862  axdc4uzlem  13897  ser1const  13972  exp0  13979  exp1  13981  expn1  13985  nn0sqcl  14003  sqval  14028  sqeq0  14034  resqcl  14038  zsqcl  14043  expubnd  14092  binom21  14133  expnbnd  14146  nn0opthlem2  14183  bcnn  14226  bcn2  14233  bcn2p1  14239  bcnm1  14241  hasheq0  14277  hashsng  14283  hashen1  14284  hashunsnggt  14308  hashin  14325  hashdif  14327  hashgt23el  14338  hashxplem  14347  hashf1lem2  14370  hash2pr  14383  hash2prde  14384  pr2pwpr  14393  hash3tr  14405  iswrd  14429  wrdval  14430  hashwrdn  14461  ccatval2  14492  ccatrid  14502  eqs1  14527  s111  14530  ccatws1len  14535  repsw0  14691  repsw1  14697  cshw0  14708  wwlktovf  14870  relexpsucnnl  14944  reim0  15032  imval2  15065  cjne0  15077  abssq  15220  max0add  15224  abs2dif  15247  rddif  15255  absrdbnd  15256  rexuz3  15263  isershft  15578  isercolllem2  15580  isercoll  15582  fsum  15634  fsumadd  15654  fsumsplitsnun  15669  bcxmas  15749  infcvgaux2i  15772  fprod  15855  risefac0  15941  fallfac0  15942  risefac1  15947  fallfac1  15948  bpoly2  15971  bpoly3  15972  bpoly4  15973  fsumcube  15974  efi4p  16053  resin4p  16054  recos4p  16055  sinbnd  16096  cosbnd  16097  rpnnen2lem8  16137  rpnnen2lem12  16141  cnso  16163  dvdsmul2  16196  dvdslelem  16227  odd2np1lem  16258  mod2eq1n2dvds  16265  divalglem0  16311  divalglem1  16312  divalglem4  16314  divalglem5  16315  divalglem8  16318  flodddiv4  16333  bits0  16346  bitsp1o  16351  bitsf1  16364  sadadd2lem2  16368  gcd1  16446  lcm0val  16512  dvdslcm  16516  lcmeq0  16518  lcmgcd  16525  lcm1  16528  lcmfunsnlem2lem2  16557  lcmfunsnlem2  16558  prm2orodd  16609  phiprm  16695  pc0  16773  pcdvdstr  16795  vdwlem2  16901  vdwlem6  16905  vdwlem8  16907  hashbc0  16924  setsval  17085  fsets  17087  setsres  17096  ressinbas  17163  ressress  17165  elrestr  17339  pwssnf1o  17410  xpsfrnel  17474  xpscf  17477  ismred2  17513  submre  17515  mreacs  17572  oppchomfval  17628  brssc  17729  isssc  17735  yonedalem4c  18191  oduleval  18203  isprs  18210  oduclatb  18421  chninf  18549  gsumval2a  18601  smndex1n0mnd  18828  mulg1  19002  mulgnegnn  19005  isghmOLD  19136  ghmghmrn  19155  cntrnsg  19264  oppgplusfval  19268  pgrpsubgsymg  19329  psgneldm2i  19425  efgrelexlemb  19670  frgp0  19680  frgpmhm  19685  vrgpf  19688  cntrcmnd  19762  cntrabl  19763  cygctb  19812  dprd0  19953  dprd2da  19964  mgpplusg  20070  opprmulfval  20266  subrngint  20484  subrgint  20519  lsp0  20951  rlmval2  21135  cncrng  21334  cnfld1  21339  zringcyg  21415  mulgrhm2  21424  zlmsca  21466  fermltlchr  21475  chrnzr  21476  zrhpsgnelbas  21540  ocvz  21624  cssincl  21634  css0  21635  css1  21636  frlmip  21724  fczpsrbag  21868  ply1idvr1OLD  22230  evls1rhmlem  22256  evl1fval1lem  22265  marrepeval  22498  decpmatid  22705  0opn  22839  topopn  22841  basdif0  22888  tgval  22890  isopn2  22967  0cld  22973  ntropn  22984  ntrval2  22986  ntrdif  22987  clsdif  22988  cmclsopn  22997  ntrtop  23005  ntr0  23016  mretopd  23027  neips  23048  neiptopnei  23067  maxlp  23082  isperf2  23087  rest0  23104  iocpnfordt  23150  icomnfordt  23151  mnfnei  23156  refref  23448  unisngl  23462  1stckgen  23489  ptbasfi  23516  pthaus  23573  fbssfi  23772  isfil2  23791  ssfg  23807  filconn  23818  fbasrn  23819  filufint  23855  imaelfm  23886  fmfnfmlem4  23892  fclsfnflim  23962  alexsubALTlem3  23984  alexsubALTlem4  23985  ustfilxp  24148  ustuqtop2  24177  ustuqtop4  24179  utopsnneiplem  24182  utopsnnei  24184  utop2nei  24185  cfiluweak  24229  neipcfilu  24230  xmetres  24299  metres  24300  mopnex  24454  prdsms  24466  metucn  24506  tngds  24583  tngngp3  24591  nmoge0  24656  cnfldnm  24713  tgioo  24731  xrtgioo  24742  xrsmopn  24748  negcncf  24862  negcncfOLD  24863  phtpy01  24931  pco0  24961  tcphtopn  25173  tchnmfval  25175  caussi  25244  rrxip  25337  minveclem3b  25375  ovolfioo  25415  ovolficc  25416  ovolfsf  25419  ovolctb  25438  ovolctb2  25440  ovolfiniun  25449  ovoliun2  25454  ovolshftlem1  25457  ovolscalem1  25461  ovolicopnf  25472  iunmbl2  25505  uniioombllem2  25531  opnmblALT  25551  ismbf  25576  mbfinf  25613  0plef  25620  itg1climres  25662  itg2cnlem1  25709  iblitg  25716  ibl0  25735  itgcn  25793  cnlimc  25836  dvfre  25902  dvnfre  25903  dveflem  25930  dvef  25931  dvlipcn  25946  lhop2  25967  itgsubstlem  26002  deg1val  26048  ply1rem  26118  coefv0  26200  plyrecj  26234  vieta1lem2  26266  aannenlem1  26283  aaliou2b  26296  ulmval  26336  ulmpm  26339  ulmdvlem1  26356  mtest  26360  efcn  26400  sin2pim  26441  cos2pim  26442  sinmpi  26443  cosmpi  26444  sinppi  26445  cosppi  26446  efimpi  26447  sincosq1lem  26453  sincosq2sgn  26455  sincosq3sgn  26456  sincosq4sgn  26457  sinq12gt0  26463  sinq34lt0t  26465  sincosq1eq  26468  abssinper  26477  efif1o  26502  loglt1b  26590  relogcn  26594  ellogdm  26595  efopn  26614  cxp0  26626  cxp1  26627  cxpsqrt  26659  logsqrt  26660  logb1  26726  atandm3  26835  atanbnd  26883  atancn  26893  leibpi  26899  efrlim  26926  efrlimOLD  26927  logdifbnd  26951  vmaprm  27074  ppip1le  27118  ppieq0  27133  prmorcht  27135  ppiublem1  27160  ppiub  27162  chpeq0  27166  chtub  27170  fsumvma  27171  pclogsum  27173  chpval2  27176  dchrresb  27217  dchrptlem1  27222  lgs0  27268  lgs2  27272  lgsdir2lem2  27284  lgsdir2lem4  27286  lgsdchrval  27312  lgsdchr  27313  lgseisenlem2  27334  2lgslem1c  27351  2lgsoddprmlem2  27367  addsq2nreurex  27402  dirith2  27486  selberg2lem  27508  qabvle  27583  qabvexp  27584  ostth  27597  noextendseq  27626  noetasuplem4  27695  noetainflem4  27699  scutun12  27771  madebdayim  27853  bdayiun  27880  addsrid  27927  addsfo  27946  peano2no  27947  negscl  27998  subsfo  28025  subsid1  28028  muls01  28071  mulsrid  28072  divs1  28163  recsex  28177  abssnid  28201  peano2ons  28232  noseqp1  28241  noseqind  28242  peano2nns  28298  n0sfincut  28302  dfnns2  28317  elzs2  28343  elnnzs  28345  elznns  28346  zsoring  28352  n0seo  28364  exps0  28370  exps1  28371  istrkg2ld  28458  istrkg3ld  28459  ttgval  28873  brbtwn  28898  colinearalglem4  28908  upgr0eop  29113  uspgrushgr  29176  usgruspgr  29179  usgr0eop  29245  0grsubgr  29277  uspgrloopvtx  29515  umgr2v2evtx  29521  usgr0edg0rusgr  29575  rgrusgrprc  29589  wlkvtxiedg  29624  pthdivtx  29726  usgr2pthlem  29762  wlkswwlksf1o  29878  wwlksext2clwwlk  30058  konigsbergssiedgw  30251  frgrncvvdeqlem7  30306  2clwwlk2  30349  ex-po  30436  pliguhgr  30487  nvnd  30689  ipval2lem3  30706  ipval2  30708  ipidsq  30711  dipcj  30715  dip0r  30718  nmlnogt0  30798  blocni  30806  ipasslem2  30833  ipasslem8  30838  ipasslem9  30839  ajval  30862  ubthlem1  30871  hvaddlid  31024  hvsub0  31077  hi02  31098  hlimi  31189  isch2  31224  chlimi  31235  chsupunss  31345  shsupunss  31347  chlejb1i  31477  h1dei  31551  h1de2ci  31557  spanunsni  31580  pjoml2i  31586  pjorthi  31670  mayete3i  31729  hosubid1  31799  nmopge0  31912  nmfnge0  31928  adj1  31934  adjeq  31936  lnop0  31967  lnopmi  32001  nmophmi  32032  cnlnadjlem5  32072  cnlnadjeui  32078  unierri  32105  leoprf2  32128  leopnmid  32139  nmopleid  32140  hstles  32232  hst0  32234  strlem3a  32253  dmdbr2  32304  mdsl1i  32322  mdsl2i  32323  mdsl2bi  32324  cvmdi  32325  mdslmd1lem1  32326  mdslmd1lem2  32327  mdslmd1i  32330  mdslmd2i  32331  csmdsymi  32335  mdexchi  32336  superpos  32355  atomli  32383  atordi  32385  chirredlem1  32391  chirredlem2  32392  atcvat4i  32398  atabsi  32402  mdsymlem1  32404  mdsymlem5  32408  mdsymlem6  32409  sumdmdii  32416  dmdbr5ati  32423  dmdbr6ati  32424  mddmdin0i  32432  cdj3lem2  32436  unidifsnel  32536  unidifsnne  32537  xppreima  32649  abfmpunirn  32656  abfmpel  32659  aciunf1lem  32666  fgreu  32676  imafi2  32717  padct  32725  fpwrelmapffslem  32739  fpwrelmap  32740  xrge0infss  32768  xrdifh  32788  indconst0  32867  indconst1  32868  pfx1s2  32949  clatp0cl  32986  clatp1cl  32987  cntrcrng  33091  cycpmco2lem4  33139  rmfsupp2  33248  1fldgenq  33332  resvval  33338  rearchi  33355  qusxpid  33372  opprabs  33491  zringfrac  33563  psrbasfsupp  33621  rlmdim  33694  constrfiss  33836  2sqr3minply  33865  locfinreflem  33925  locfinref  33926  ordtconnlem1  34009  rge0scvg  34034  lmxrge0  34037  qqh0  34069  qqh1  34070  rrh0  34100  zrhre  34104  esumcst  34148  esumfzf  34154  esumfsupre  34156  hasheuni  34170  sgon  34209  dmvlsiga  34214  sigainb  34221  measval  34283  ismeas  34284  sxbrsigalem0  34356  omssubadd  34385  carsggect  34403  eulerpartlemmf  34460  eulerpartlemgs2  34465  eulerpartlemn  34466  rrvsum  34539  ballotlem2  34574  ballotlemfcc  34579  ballotlem4  34584  signsplypnf  34635  signsply0  34636  signsw0glem  34638  signswrid  34643  signlem0  34672  signshf  34673  bnj535  34974  bnj580  34997  bnj907  35051  bnj1253  35101  funen1cnv  35172  rankval4b  35183  fineqvnttrclse  35216  onvf1odlem1  35219  onvf1od  35223  loop1cycl  35253  ptpconn  35349  cvmsss2  35390  cvmlift2lem12  35430  cvmlift2lem13  35431  cvmliftphtlem  35433  cvmliftpht  35434  fmlafvel  35501  mppsthm  35695  bcneg1  35852  fv1stcnv  35893  fv2ndcnv  35894  wlimeq1  35934  imagesset  36069  altopeq1  36079  brcolinear2  36174  cldbnd  36442  ivthALT  36451  refssfne  36474  ontgval  36547  onint1  36565  axc11n11r  36800  bj-pm11.53a  36895  bj-bm1.3ii  37181  bj-restsn0  37202  bj-restsn10  37203  bj-restsnid  37204  bj-rest10  37205  bj-rest0  37210  bj-inftyexpiinv  37325  bj-inftyexpidisj  37327  taupilem1  37438  irrdiff  37443  f1omptsnlem  37453  mptsnunlem  37455  topdifinffinlem  37464  inunissunidif  37492  rdgssun  37495  exrecfnlem  37496  exrecfnpw  37498  finixpnum  37718  tan2h  37725  matunitlindflem2  37730  ptrest  37732  poimirlem22  37755  poimirlem25  37758  mblfinlem1  37770  mblfinlem2  37771  mblfinlem3  37772  mblfinlem4  37773  ismblfin  37774  itg2addnclem  37784  itg2addnclem2  37785  itg2addnclem3  37786  itg2addnc  37787  itg2gt0cn  37788  ftc1anclem5  37810  ftc1anclem8  37813  dvasin  37817  dvacos  37818  sdclem2  37855  totbndbnd  37902  heibor1lem  37922  heiborlem7  37930  bfplem1  37935  prnc  38180  brxrn  38480  ecxrn2  38505  riotasv  39131  glbconN  39549  atpointN  39915  polsubN  40079  pol0N  40081  pol1N  40082  2polvalN  40086  2polssN  40087  3polN  40088  pcl0N  40094  2pmaplubN  40098  pnonsingN  40105  polsubclN  40124  cdlemefs32sn1aw  40586  cdleme43fsv1snlem  40592  cdleme41sn3a  40605  cdleme32a  40613  cdleme40m  40639  cdleme40n  40640  cdleme42b  40650  istendo  40932  cdlemk40  41089  cdlemkid  41108  dihvalcqpre  41407  facp2  42309  relt0neg1  42626  sn-nnne0  42630  frlmsnic  42710  prjspnerlem  42775  prjspnval2  42776  0prjspn  42786  3cubes  42847  mapfzcons1cl  42875  eldioph3b  42922  eldiophss  42931  0dioph  42935  vdioph  42936  eldioph4b  42968  eldioph4i  42969  rencldnfilem  42977  rmxy1  43079  rmxy0  43080  rmxm1  43091  rmym1  43092  monotoddzzfi  43099  wepwso  43200  aomclem6  43216  pwslnmlem0  43248  isnumbasabl  43263  areaquad  43373  onexlimgt  43400  oaabsb  43451  nadd1suc  43549  om2  43561  oe2  43563  safesnsupfidom1o  43574  onno  43590  oa1cl  43604  finona1cl  43610  reabsifneg  43789  reabsifnneg  43792  relexp2  43834  eltrclrec  43837  elrtrclrec  43838  brtrclrec  43853  brrtrclrec  43854  relexpxpmin  43874  dftrcl3  43877  dfrtrcl3  43890  heeq1  43934  seff  44466  lhe4.4ex1a  44486  eelT0  44931  snssl  44986  sineq0ALT  45093  trfr  45119  xpwf  45121  dmwf  45122  rnwf  45123  modelaxreplem1  45135  modelaxreplem3  45137  0elaxnul  45140  prclaxpr  45142  uniclaxun  45143  wfac8prim  45159  permaxinf2lem  45169  elrnmpt1sf  45349  founiiun0  45350  supxrgere  45494  supxrgelem  45498  fmuldfeqlem1  45744  fmuldfeq  45745  climneg  45772  sumnnodd  45792  liminfltlem  45964  xlimpnfxnegmnf2  46018  addccncf2  46036  dvsinax  46073  stoweidlem18  46178  stoweidlem19  46179  stoweidlem22  46182  stoweidlem34  46194  stoweidlem40  46200  stoweidlem41  46201  stoweidlem55  46215  stoweidlem59  46219  dirker2re  46252  dirkerdenne0  46253  fourierdlem48  46314  fourierdlem49  46315  fourierdlem70  46336  fourierdlem71  46337  fourierdlem104  46370  fourierdlem112  46378  fouriersw  46391  etransclem46  46440  etransclem48  46442  nnfoctbdjlem  46615  ormklocald  47034  natlocalincr  47036  cjnpoly  47051  sinnpoly  47053  sqrtnegnre  47469  fsummmodsnunz  47537  flsqrt5  47756  bits0ALTV  47841  mogoldbblem  47882  sgoldbeven3prm  47945  nnsum3primes4  47950  isubgr0uhgr  48035  ushggricedg  48089  2zrngnmlid  48417  2zrngnmrid  48418  mpoexxg2  48500  lco0  48589  zlmodzxzldeplem3  48664  0dig1  48771  naryfvalel  48792  ackvalsuc0val  48849  iinxp  48992  0funclem  49247  aacllem  49962