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  3442  elabg  3632  eueq2  3669  sbcgf  3812  sbcralg  3825  csbconstgf  3868  sbcnestgw  4373  csbnestgw  4374  sbcnestg  4378  csbnestg  4379  csbnest1g  4382  iinexg  5286  eusv2nf  5333  reusv2lem5  5340  nnullss  5402  xpss1  5635  xpiindi  5775  reldm0  5868  elrnmpt1s  5899  resdm  5975  eliniseg  6043  trinxp  6072  ssrnres  6125  cnveq0  6144  coi2  6211  relrelss  6220  cnviin  6233  elpred  6265  onelssex  6355  ord0eln0  6362  funcnvres  6559  funimaex  6569  fnresin1  6606  fnresin2  6607  fresin  6692  ssimaex  6907  fvmpt  6929  fvmptnf  6951  fvimacnvALT  6990  dff3  7033  fsn  7068  fsn2  7069  funop  7082  fvrnressn  7094  fnsnbg  7098  fninfp  7108  fndifnfp  7110  fnnfpeq0  7112  fprb  7128  elabrex  7176  elabrexg  7177  f1elima  7197  f1ofvswap  7240  fliftel1  7244  f1owe  7287  sorpssuni  7665  sorpssint  7666  eldifpw  7701  ordeleqon  7715  ordsson  7716  ssnlim  7816  abrexexg  7893  tposfun  8172  tpostpos2  8177  fpr3g  8215  wfr3g  8249  tfrlem10  8306  tfrlem12  8308  tfr3  8318  seqomlem1  8369  seqomlem2  8370  seqomlem4  8372  ondif2  8417  oa0  8431  om0  8432  oa1suc  8446  om1  8457  oe1  8459  oe1m  8460  omass  8495  oeoalem  8511  oeoelem  8513  nnmsucr  8540  nnm1  8567  nnm2  8568  naddrid  8598  naddlid  8599  ecelqs  8692  xpider  8712  mapdm0  8766  fvdiagfn  8815  ixpsnf1o  8862  xp1en  8976  undom  8978  sbthlem7  9006  domunsn  9040  xpmapenlem  9057  infensuc  9068  findcard2d  9076  diffi  9084  cnvfi  9085  enreffi  9092  snnen2o  9129  1sdom2dom  9138  infi  9154  finresfin  9156  unblem1  9176  unblem2  9177  unblem3  9178  unblem4  9179  isfinite2  9182  infn0ALT  9187  unfilem1  9189  unfilem2  9190  unfir  9192  fofinf1o  9216  cnvfiALT  9223  mptfi  9235  finsschain  9243  marypha2  9323  inf0  9511  trcl  9618  frr3g  9649  r1rankidb  9697  snwf  9702  unwf  9703  uniwf  9712  rankval3b  9719  rankr1a  9729  rankxplim3  9774  scott0  9779  djueq1  9798  card1  9861  pm54.43  9894  infxpenc2  9913  dfac8clem  9923  alephsuc2  9971  alephle  9979  cardaleph  9980  dfac12lem2  10036  undjudom  10059  djudom1  10074  pwdju1  10082  nnadju  10089  ackbij1lem18  10127  cflem  10136  cflemOLD  10137  cflecard  10144  cfeq0  10147  cfslb  10157  cfsmolem  10161  cfcoflem  10163  cfidm  10166  isfin4p1  10206  fin23lem12  10222  fin23lem16  10226  fin23lem28  10231  fin23lem38  10240  fin23lem41  10243  fin1a2lem7  10297  fin1a2lem12  10302  fin1a2lem13  10303  hsmexlem8  10315  axcc2lem  10327  axcc3  10329  domtriomlem  10333  axdc3lem2  10342  axdc3lem4  10344  axdc4lem  10346  axcclem  10348  ac6num  10370  ttukeylem4  10403  ttukeylem7  10406  ttukey2g  10407  axdclem  10410  brdom3  10419  brdom5  10420  cardeq0  10443  unsnen  10444  konigthlem  10459  pwcfsdom  10474  canthp1lem1  10543  wunex2  10629  wuncval2  10638  eltsk2g  10642  ingru  10706  grutsk  10713  axgroth6  10719  mulidpi  10777  nlt1pi  10797  indpi  10798  pinq  10818  mulidnq  10854  1idpr  10920  prlem934  10924  0idsr  10988  1idsr  10989  00sr  10990  negexsr  10993  recexsrlem  10994  sqgt0sr  10997  ax1rid  11052  axcnre  11055  ne0gt0  11218  peano2cn  11285  peano2re  11286  00id  11288  mul02lem2  11290  mul01  11292  subid  11380  subid1  11381  negid  11408  negeq0  11415  peano2cnm  11427  peano2rem  11428  lt0neg1  11623  le0neg1  11625  relin01  11641  div2neg  11844  recgt0ii  12028  divgt0i2i  12037  ledivp1i  12047  ltdivp1i  12048  inelr  12115  peano5nni  12128  peano2nn  12137  nnge1  12153  nnne0  12159  times2  12257  addltmul  12357  nn0p1nn  12420  peano2nn0  12421  nn0lele2xi  12437  fcdmnn0supp  12438  fcdmnn0fsupp  12439  fcdmnn0suppg  12440  peano2z  12513  peano2zm  12515  suprzcl  12553  zeo  12559  eluzaddi  12763  uzwo  12809  uzwo2  12810  infssuzle  12829  infssuzcl  12830  zq  12852  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem5  12879  rphalfcl  12919  zgt1rpn0n1  12933  ltpnf  13019  nltmnf  13028  pnfge  13029  nltpnft  13063  xlemnf  13066  qsqueeze  13100  xlt0neg1  13118  xle0neg1  13120  xaddpnf1  13125  xaddmnf1  13127  xaddrid  13140  xsubge0  13160  xmul01  13166  xmulneg1  13168  xmulpnf1  13173  xmulrid  13178  supxrbnd  13227  supxrgtmnf  13228  supxrre1  13229  supxrre2  13230  elioopnf  13343  elicopnf  13345  iccshftri  13387  iccshftli  13389  iccdili  13391  icccntri  13393  fzprval  13485  fz0add1fz1  13635  fzofzp1  13664  fzostep1  13686  injresinj  13691  flge0nn0  13724  flge1nn  13725  btwnzge0  13732  modfrac  13788  om2uzsuci  13855  axdc4uzlem  13890  ser1const  13965  exp0  13972  exp1  13974  expn1  13978  nn0sqcl  13996  sqval  14021  sqeq0  14027  resqcl  14031  zsqcl  14036  expubnd  14085  binom21  14126  expnbnd  14139  nn0opthlem2  14176  bcnn  14219  bcn2  14226  bcn2p1  14232  bcnm1  14234  hasheq0  14270  hashsng  14276  hashen1  14277  hashunsnggt  14301  hashin  14318  hashdif  14320  hashgt23el  14331  hashxplem  14340  hashf1lem2  14363  hash2pr  14376  hash2prde  14377  pr2pwpr  14386  hash3tr  14398  iswrd  14422  wrdval  14423  hashwrdn  14454  ccatval2  14485  ccatrid  14495  eqs1  14520  s111  14523  ccatws1len  14528  repsw0  14684  repsw1  14690  cshw0  14701  wwlktovf  14863  relexpsucnnl  14937  reim0  15025  imval2  15058  cjne0  15070  abssq  15213  max0add  15217  abs2dif  15240  rddif  15248  absrdbnd  15249  rexuz3  15256  isershft  15571  isercolllem2  15573  isercoll  15575  fsum  15627  fsumadd  15647  fsumsplitsnun  15662  bcxmas  15742  infcvgaux2i  15765  fprod  15848  risefac0  15934  fallfac0  15935  risefac1  15940  fallfac1  15941  bpoly2  15964  bpoly3  15965  bpoly4  15966  fsumcube  15967  efi4p  16046  resin4p  16047  recos4p  16048  sinbnd  16089  cosbnd  16090  rpnnen2lem8  16130  rpnnen2lem12  16134  cnso  16156  dvdsmul2  16189  dvdslelem  16220  odd2np1lem  16251  mod2eq1n2dvds  16258  divalglem0  16304  divalglem1  16305  divalglem4  16307  divalglem5  16308  divalglem8  16311  flodddiv4  16326  bits0  16339  bitsp1o  16344  bitsf1  16357  sadadd2lem2  16361  gcd1  16439  lcm0val  16505  dvdslcm  16509  lcmeq0  16511  lcmgcd  16518  lcm1  16521  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  prm2orodd  16602  phiprm  16688  pc0  16766  pcdvdstr  16788  vdwlem2  16894  vdwlem6  16898  vdwlem8  16900  hashbc0  16917  setsval  17078  fsets  17080  setsres  17089  ressinbas  17156  ressress  17158  elrestr  17332  pwssnf1o  17402  xpsfrnel  17466  xpscf  17469  ismred2  17505  submre  17507  mreacs  17564  oppchomfval  17620  brssc  17721  isssc  17727  yonedalem4c  18183  oduleval  18195  isprs  18202  oduclatb  18413  chninf  18541  gsumval2a  18593  smndex1n0mnd  18820  mulg1  18994  mulgnegnn  18997  isghmOLD  19129  ghmghmrn  19148  cntrnsg  19257  oppgplusfval  19261  pgrpsubgsymg  19322  psgneldm2i  19418  efgrelexlemb  19663  frgp0  19673  frgpmhm  19678  vrgpf  19681  cntrcmnd  19755  cntrabl  19756  cygctb  19805  dprd0  19946  dprd2da  19957  mgpplusg  20063  opprmulfval  20258  subrngint  20476  subrgint  20511  lsp0  20943  rlmval2  21127  cncrng  21326  cnfld1  21331  zringcyg  21407  mulgrhm2  21416  zlmsca  21458  fermltlchr  21467  chrnzr  21468  zrhpsgnelbas  21532  ocvz  21616  cssincl  21626  css0  21627  css1  21628  frlmip  21716  fczpsrbag  21859  ply1idvr1OLD  22211  evls1rhmlem  22237  evl1fval1lem  22246  marrepeval  22479  decpmatid  22686  0opn  22820  topopn  22822  basdif0  22869  tgval  22871  isopn2  22948  0cld  22954  ntropn  22965  ntrval2  22967  ntrdif  22968  clsdif  22969  cmclsopn  22978  ntrtop  22986  ntr0  22997  mretopd  23008  neips  23029  neiptopnei  23048  maxlp  23063  isperf2  23068  rest0  23085  iocpnfordt  23131  icomnfordt  23132  mnfnei  23137  refref  23429  unisngl  23443  1stckgen  23470  ptbasfi  23497  pthaus  23554  fbssfi  23753  isfil2  23772  ssfg  23788  filconn  23799  fbasrn  23800  filufint  23836  imaelfm  23867  fmfnfmlem4  23873  fclsfnflim  23943  alexsubALTlem3  23965  alexsubALTlem4  23966  ustfilxp  24129  ustuqtop2  24158  ustuqtop4  24160  utopsnneiplem  24163  utopsnnei  24165  utop2nei  24166  cfiluweak  24210  neipcfilu  24211  xmetres  24280  metres  24281  mopnex  24435  prdsms  24447  metucn  24487  tngds  24564  tngngp3  24572  nmoge0  24637  cnfldnm  24694  tgioo  24712  xrtgioo  24723  xrsmopn  24729  negcncf  24843  negcncfOLD  24844  phtpy01  24912  pco0  24942  tcphtopn  25154  tchnmfval  25156  caussi  25225  rrxip  25318  minveclem3b  25356  ovolfioo  25396  ovolficc  25397  ovolfsf  25400  ovolctb  25419  ovolctb2  25421  ovolfiniun  25430  ovoliun2  25435  ovolshftlem1  25438  ovolscalem1  25442  ovolicopnf  25453  iunmbl2  25486  uniioombllem2  25512  opnmblALT  25532  ismbf  25557  mbfinf  25594  0plef  25601  itg1climres  25643  itg2cnlem1  25690  iblitg  25697  ibl0  25716  itgcn  25774  cnlimc  25817  dvfre  25883  dvnfre  25884  dveflem  25911  dvef  25912  dvlipcn  25927  lhop2  25948  itgsubstlem  25983  deg1val  26029  ply1rem  26099  coefv0  26181  plyrecj  26215  vieta1lem2  26247  aannenlem1  26264  aaliou2b  26277  ulmval  26317  ulmpm  26320  ulmdvlem1  26337  mtest  26341  efcn  26381  sin2pim  26422  cos2pim  26423  sinmpi  26424  cosmpi  26425  sinppi  26426  cosppi  26427  efimpi  26428  sincosq1lem  26434  sincosq2sgn  26436  sincosq3sgn  26437  sincosq4sgn  26438  sinq12gt0  26444  sinq34lt0t  26446  sincosq1eq  26449  abssinper  26458  efif1o  26483  loglt1b  26571  relogcn  26575  ellogdm  26576  efopn  26595  cxp0  26607  cxp1  26608  cxpsqrt  26640  logsqrt  26641  logb1  26707  atandm3  26816  atanbnd  26864  atancn  26874  leibpi  26880  efrlim  26907  efrlimOLD  26908  logdifbnd  26932  vmaprm  27055  ppip1le  27099  ppieq0  27114  prmorcht  27116  ppiublem1  27141  ppiub  27143  chpeq0  27147  chtub  27151  fsumvma  27152  pclogsum  27154  chpval2  27157  dchrresb  27198  dchrptlem1  27203  lgs0  27249  lgs2  27253  lgsdir2lem2  27265  lgsdir2lem4  27267  lgsdchrval  27293  lgsdchr  27294  lgseisenlem2  27315  2lgslem1c  27332  2lgsoddprmlem2  27348  addsq2nreurex  27383  dirith2  27467  selberg2lem  27489  qabvle  27564  qabvexp  27565  ostth  27578  noextendseq  27607  noetasuplem4  27676  noetainflem4  27680  scutun12  27752  madebdayim  27834  bdayiun  27861  addsrid  27908  addsfo  27927  peano2no  27928  negscl  27979  subsfo  28006  subsid1  28009  muls01  28052  mulsrid  28053  divs1  28144  recsex  28158  abssnid  28182  peano2ons  28213  noseqp1  28222  noseqind  28223  peano2nns  28279  n0sfincut  28283  dfnns2  28298  elzs2  28324  elnnzs  28326  elznns  28327  zsoring  28333  n0seo  28345  exps0  28351  exps1  28352  istrkg2ld  28439  istrkg3ld  28440  ttgval  28854  brbtwn  28878  colinearalglem4  28888  upgr0eop  29093  uspgrushgr  29156  usgruspgr  29159  usgr0eop  29225  0grsubgr  29257  uspgrloopvtx  29495  umgr2v2evtx  29501  usgr0edg0rusgr  29555  rgrusgrprc  29569  wlkvtxiedg  29604  pthdivtx  29706  usgr2pthlem  29742  wlkswwlksf1o  29858  wwlksext2clwwlk  30035  konigsbergssiedgw  30228  frgrncvvdeqlem7  30283  2clwwlk2  30326  ex-po  30413  pliguhgr  30464  nvnd  30666  ipval2lem3  30683  ipval2  30685  ipidsq  30688  dipcj  30692  dip0r  30695  nmlnogt0  30775  blocni  30783  ipasslem2  30810  ipasslem8  30815  ipasslem9  30816  ajval  30839  ubthlem1  30848  hvaddlid  31001  hvsub0  31054  hi02  31075  hlimi  31166  isch2  31201  chlimi  31212  chsupunss  31322  shsupunss  31324  chlejb1i  31454  h1dei  31528  h1de2ci  31534  spanunsni  31557  pjoml2i  31563  pjorthi  31647  mayete3i  31706  hosubid1  31776  nmopge0  31889  nmfnge0  31905  adj1  31911  adjeq  31913  lnop0  31944  lnopmi  31978  nmophmi  32009  cnlnadjlem5  32049  cnlnadjeui  32055  unierri  32082  leoprf2  32105  leopnmid  32116  nmopleid  32117  hstles  32209  hst0  32211  strlem3a  32230  dmdbr2  32281  mdsl1i  32299  mdsl2i  32300  mdsl2bi  32301  cvmdi  32302  mdslmd1lem1  32303  mdslmd1lem2  32304  mdslmd1i  32307  mdslmd2i  32308  csmdsymi  32312  mdexchi  32313  superpos  32332  atomli  32360  atordi  32362  chirredlem1  32368  chirredlem2  32369  atcvat4i  32375  atabsi  32379  mdsymlem1  32381  mdsymlem5  32385  mdsymlem6  32386  sumdmdii  32393  dmdbr5ati  32400  dmdbr6ati  32401  mddmdin0i  32409  cdj3lem2  32413  unidifsnel  32513  unidifsnne  32514  xppreima  32625  abfmpunirn  32632  abfmpel  32635  aciunf1lem  32642  fgreu  32652  imafi2  32691  padct  32699  fpwrelmapffslem  32713  fpwrelmap  32714  xrge0infss  32741  xrdifh  32761  pfx1s2  32918  clatp0cl  32955  clatp1cl  32956  cntrcrng  33048  cycpmco2lem4  33096  rmfsupp2  33203  1fldgenq  33286  resvval  33292  rearchi  33309  qusxpid  33326  opprabs  33445  zringfrac  33517  psrbasfsupp  33570  rlmdim  33620  constrfiss  33762  2sqr3minply  33791  locfinreflem  33851  locfinref  33852  ordtconnlem1  33935  rge0scvg  33960  lmxrge0  33963  qqh0  33995  qqh1  33996  rrh0  34026  zrhre  34030  esumcst  34074  esumfzf  34080  esumfsupre  34082  hasheuni  34096  sgon  34135  dmvlsiga  34140  sigainb  34147  measval  34209  ismeas  34210  sxbrsigalem0  34282  omssubadd  34311  carsggect  34329  eulerpartlemmf  34386  eulerpartlemgs2  34391  eulerpartlemn  34392  rrvsum  34465  ballotlem2  34500  ballotlemfcc  34505  ballotlem4  34510  signsplypnf  34561  signsply0  34562  signsw0glem  34564  signswrid  34569  signlem0  34598  signshf  34599  bnj535  34900  bnj580  34923  bnj907  34977  bnj1253  35027  funen1cnv  35098  rankval4b  35109  fineqvnttrclse  35142  onvf1odlem1  35145  onvf1od  35149  loop1cycl  35179  ptpconn  35275  cvmsss2  35316  cvmlift2lem12  35356  cvmlift2lem13  35357  cvmliftphtlem  35359  cvmliftpht  35360  fmlafvel  35427  mppsthm  35621  bcneg1  35778  fv1stcnv  35819  fv2ndcnv  35820  wlimeq1  35860  imagesset  35993  altopeq1  36003  brcolinear2  36098  cldbnd  36366  ivthALT  36375  refssfne  36398  ontgval  36471  onint1  36489  axc11n11r  36723  bj-pm11.53a  36818  bj-bm1.3ii  37104  bj-restsn0  37125  bj-restsn10  37126  bj-restsnid  37127  bj-rest10  37128  bj-rest0  37133  bj-inftyexpiinv  37248  bj-inftyexpidisj  37250  taupilem1  37361  irrdiff  37366  f1omptsnlem  37376  mptsnunlem  37378  topdifinffinlem  37387  inunissunidif  37415  rdgssun  37418  exrecfnlem  37419  exrecfnpw  37421  finixpnum  37651  tan2h  37658  matunitlindflem2  37663  ptrest  37665  poimirlem22  37688  poimirlem25  37691  mblfinlem1  37703  mblfinlem2  37704  mblfinlem3  37705  mblfinlem4  37706  ismblfin  37707  itg2addnclem  37717  itg2addnclem2  37718  itg2addnclem3  37719  itg2addnc  37720  itg2gt0cn  37721  ftc1anclem5  37743  ftc1anclem8  37746  dvasin  37750  dvacos  37751  sdclem2  37788  totbndbnd  37835  heibor1lem  37855  heiborlem7  37863  bfplem1  37868  prnc  38113  brxrn  38408  riotasv  39004  glbconN  39422  atpointN  39788  polsubN  39952  pol0N  39954  pol1N  39955  2polvalN  39959  2polssN  39960  3polN  39961  pcl0N  39967  2pmaplubN  39971  pnonsingN  39978  polsubclN  39997  cdlemefs32sn1aw  40459  cdleme43fsv1snlem  40465  cdleme41sn3a  40478  cdleme32a  40486  cdleme40m  40512  cdleme40n  40513  cdleme42b  40523  istendo  40805  cdlemk40  40962  cdlemkid  40981  dihvalcqpre  41280  facp2  42182  relt0neg1  42495  sn-nnne0  42499  frlmsnic  42579  prjspnerlem  42656  prjspnval2  42657  0prjspn  42667  3cubes  42729  mapfzcons1cl  42757  eldioph3b  42804  eldiophss  42813  0dioph  42817  vdioph  42818  eldioph4b  42850  eldioph4i  42851  rencldnfilem  42859  rmxy1  42961  rmxy0  42962  rmxm1  42973  rmym1  42974  monotoddzzfi  42981  wepwso  43082  aomclem6  43098  pwslnmlem0  43130  isnumbasabl  43145  areaquad  43255  onexlimgt  43282  oaabsb  43333  nadd1suc  43431  om2  43443  oe2  43445  safesnsupfidom1o  43456  onno  43472  oa1cl  43486  finona1cl  43492  reabsifneg  43671  reabsifnneg  43674  relexp2  43716  eltrclrec  43719  elrtrclrec  43720  brtrclrec  43735  brrtrclrec  43736  relexpxpmin  43756  dftrcl3  43759  dfrtrcl3  43772  heeq1  43816  seff  44348  lhe4.4ex1a  44368  eelT0  44813  snssl  44868  sineq0ALT  44975  trfr  45001  xpwf  45003  dmwf  45004  rnwf  45005  modelaxreplem1  45017  modelaxreplem3  45019  0elaxnul  45022  prclaxpr  45024  uniclaxun  45025  wfac8prim  45041  permaxinf2lem  45051  elrnmpt1sf  45232  founiiun0  45233  supxrgere  45378  supxrgelem  45382  fmuldfeqlem1  45628  fmuldfeq  45629  climneg  45656  sumnnodd  45676  liminfltlem  45848  xlimpnfxnegmnf2  45902  addccncf2  45920  dvsinax  45957  stoweidlem18  46062  stoweidlem19  46063  stoweidlem22  46066  stoweidlem34  46078  stoweidlem40  46084  stoweidlem41  46085  stoweidlem55  46099  stoweidlem59  46103  dirker2re  46136  dirkerdenne0  46137  fourierdlem48  46198  fourierdlem49  46199  fourierdlem70  46220  fourierdlem71  46221  fourierdlem104  46254  fourierdlem112  46262  fouriersw  46275  etransclem46  46324  etransclem48  46326  nnfoctbdjlem  46499  ormklocald  46918  natlocalincr  46920  cjnpoly  46926  sinnpoly  46928  sqrtnegnre  47344  fsummmodsnunz  47412  flsqrt5  47631  bits0ALTV  47716  mogoldbblem  47757  sgoldbeven3prm  47820  nnsum3primes4  47825  isubgr0uhgr  47910  ushggricedg  47964  2zrngnmlid  48292  2zrngnmrid  48293  mpoexxg2  48375  lco0  48465  zlmodzxzldeplem3  48540  0dig1  48647  naryfvalel  48668  ackvalsuc0val  48725  iinxp  48868  0funclem  49124  aacllem  49839