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  3456  elabg  3646  eueq2  3684  sbcgf  3827  sbcralg  3840  csbconstgf  3883  sbcnestgw  4389  csbnestgw  4390  sbcnestg  4394  csbnestg  4395  csbnest1g  4398  iinexg  5306  eusv2nf  5353  reusv2lem5  5360  nnullss  5425  xpss1  5660  xpiindi  5802  reldm0  5894  elrnmpt1s  5926  resdm  6000  eliniseg  6068  trinxp  6101  ssrnres  6154  cnveq0  6173  coi2  6239  relrelss  6249  cnviin  6262  elpred  6294  onelssex  6384  ord0eln0  6391  funcnvres  6597  funimaex  6608  fnresin1  6646  fnresin2  6647  fresin  6732  ssimaex  6949  fvmpt  6971  fvmptnf  6993  fvimacnvALT  7032  dff3  7075  fsn  7110  fsn2  7111  funop  7124  fvrnressn  7136  fnsnbg  7141  fninfp  7151  fndifnfp  7153  fnnfpeq0  7155  fprb  7171  elabrex  7219  elabrexg  7220  f1elima  7241  f1ofvswap  7284  fliftel1  7288  f1owe  7331  sorpssuni  7711  sorpssint  7712  eldifpw  7747  ordeleqon  7761  ordsson  7762  ssnlim  7865  abrexexg  7942  tposfun  8224  tpostpos2  8229  fpr3g  8267  wfr3g  8301  tfrlem10  8358  tfrlem12  8360  tfr3  8370  seqomlem1  8421  seqomlem2  8422  seqomlem4  8424  ondif2  8469  oa0  8483  om0  8484  oa1suc  8498  om1  8509  oe1  8511  oe1m  8512  omass  8547  oeoalem  8563  oeoelem  8565  nnmsucr  8592  nnm1  8619  nnm2  8620  naddrid  8650  naddlid  8651  ecelqs  8744  xpider  8764  mapdm0  8818  fvdiagfn  8867  ixpsnf1o  8914  xp1en  9031  undom  9033  sbthlem7  9063  domunsn  9097  xpmapenlem  9114  infensuc  9125  findcard2d  9136  diffi  9145  cnvfi  9146  enreffi  9153  snnen2o  9191  1sdom2dom  9201  infi  9220  finresfin  9222  unblem1  9246  unblem2  9247  unblem3  9248  unblem4  9249  isfinite2  9252  infn0ALT  9259  unfilem1  9261  unfilem2  9262  unfir  9264  fofinf1o  9290  cnvfiALT  9297  mptfi  9309  finsschain  9317  marypha2  9397  inf0  9581  trcl  9688  frr3g  9716  r1rankidb  9764  snwf  9769  unwf  9770  uniwf  9779  rankval3b  9786  rankr1a  9796  rankxplim3  9841  scott0  9846  djueq1  9865  card1  9928  pm54.43  9961  infxpenc2  9982  dfac8clem  9992  alephsuc2  10040  alephle  10048  cardaleph  10049  dfac12lem2  10105  undjudom  10128  djudom1  10143  pwdju1  10151  nnadju  10158  ackbij1lem18  10196  cflem  10205  cflemOLD  10206  cflecard  10213  cfeq0  10216  cfslb  10226  cfsmolem  10230  cfcoflem  10232  cfidm  10235  isfin4p1  10275  fin23lem12  10291  fin23lem16  10295  fin23lem28  10300  fin23lem38  10309  fin23lem41  10312  fin1a2lem7  10366  fin1a2lem12  10371  fin1a2lem13  10372  hsmexlem8  10384  axcc2lem  10396  axcc3  10398  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  ac6num  10439  ttukeylem4  10472  ttukeylem7  10475  ttukey2g  10476  axdclem  10479  brdom3  10488  brdom5  10489  cardeq0  10512  unsnen  10513  konigthlem  10528  pwcfsdom  10543  canthp1lem1  10612  wunex2  10698  wuncval2  10707  eltsk2g  10711  ingru  10775  grutsk  10782  axgroth6  10788  mulidpi  10846  nlt1pi  10866  indpi  10867  pinq  10887  mulidnq  10923  1idpr  10989  prlem934  10993  0idsr  11057  1idsr  11058  00sr  11059  negexsr  11062  recexsrlem  11063  sqgt0sr  11066  ax1rid  11121  axcnre  11124  ne0gt0  11286  peano2cn  11353  peano2re  11354  00id  11356  mul02lem2  11358  mul01  11360  subid  11448  subid1  11449  negid  11476  negeq0  11483  peano2cnm  11495  peano2rem  11496  lt0neg1  11691  le0neg1  11693  relin01  11709  div2neg  11912  recgt0ii  12096  divgt0i2i  12105  ledivp1i  12115  ltdivp1i  12116  inelr  12183  peano5nni  12196  peano2nn  12205  nnge1  12221  nnne0  12227  times2  12325  addltmul  12425  nn0p1nn  12488  peano2nn0  12489  nn0lele2xi  12505  fcdmnn0supp  12506  fcdmnn0fsupp  12507  fcdmnn0suppg  12508  peano2z  12581  peano2zm  12583  suprzcl  12621  zeo  12627  eluzaddi  12831  uzwo  12877  uzwo2  12878  infssuzle  12897  infssuzcl  12898  zq  12920  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  rphalfcl  12987  zgt1rpn0n1  13001  ltpnf  13087  nltmnf  13096  pnfge  13097  nltpnft  13131  xlemnf  13134  qsqueeze  13168  xlt0neg1  13186  xle0neg1  13188  xaddpnf1  13193  xaddmnf1  13195  xaddrid  13208  xsubge0  13228  xmul01  13234  xmulneg1  13236  xmulpnf1  13241  xmulrid  13246  supxrbnd  13295  supxrgtmnf  13296  supxrre1  13297  supxrre2  13298  elioopnf  13411  elicopnf  13413  iccshftri  13455  iccshftli  13457  iccdili  13459  icccntri  13461  fzprval  13553  fz0add1fz1  13703  fzofzp1  13732  fzostep1  13751  injresinj  13756  flge0nn0  13789  flge1nn  13790  btwnzge0  13797  modfrac  13853  om2uzsuci  13920  axdc4uzlem  13955  ser1const  14030  exp0  14037  exp1  14039  expn1  14043  nn0sqcl  14061  sqval  14086  sqeq0  14092  resqcl  14096  zsqcl  14101  expubnd  14150  binom21  14191  expnbnd  14204  nn0opthlem2  14241  bcnn  14284  bcn2  14291  bcn2p1  14297  bcnm1  14299  hasheq0  14335  hashsng  14341  hashen1  14342  hashunsnggt  14366  hashin  14383  hashdif  14385  hashgt23el  14396  hashxplem  14405  hashf1lem2  14428  hash2pr  14441  hash2prde  14442  pr2pwpr  14451  hash3tr  14463  iswrd  14487  wrdval  14488  hashwrdn  14519  ccatval2  14550  ccatrid  14559  eqs1  14584  s111  14587  ccatws1len  14592  repsw0  14749  repsw1  14755  cshw0  14766  wwlktovf  14929  relexpsucnnl  15003  reim0  15091  imval2  15124  cjne0  15136  abssq  15279  max0add  15283  abs2dif  15306  rddif  15314  absrdbnd  15315  rexuz3  15322  isershft  15637  isercolllem2  15639  isercoll  15641  fsum  15693  fsumadd  15713  fsumsplitsnun  15728  bcxmas  15808  infcvgaux2i  15831  fprod  15914  risefac0  16000  fallfac0  16001  risefac1  16006  fallfac1  16007  bpoly2  16030  bpoly3  16031  bpoly4  16032  fsumcube  16033  efi4p  16112  resin4p  16113  recos4p  16114  sinbnd  16155  cosbnd  16156  rpnnen2lem8  16196  rpnnen2lem12  16200  cnso  16222  dvdsmul2  16255  dvdslelem  16286  odd2np1lem  16317  mod2eq1n2dvds  16324  divalglem0  16370  divalglem1  16371  divalglem4  16373  divalglem5  16374  divalglem8  16377  flodddiv4  16392  bits0  16405  bitsp1o  16410  bitsf1  16423  sadadd2lem2  16427  gcd1  16505  lcm0val  16571  dvdslcm  16575  lcmeq0  16577  lcmgcd  16584  lcm1  16587  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  prm2orodd  16668  phiprm  16754  pc0  16832  pcdvdstr  16854  vdwlem2  16960  vdwlem6  16964  vdwlem8  16966  hashbc0  16983  setsval  17144  fsets  17146  setsres  17155  ressinbas  17222  ressress  17224  elrestr  17398  pwssnf1o  17468  xpsfrnel  17532  xpscf  17535  ismred2  17571  submre  17573  mreacs  17626  oppchomfval  17682  brssc  17783  isssc  17789  yonedalem4c  18245  oduleval  18257  isprs  18264  oduclatb  18473  gsumval2a  18619  smndex1n0mnd  18846  mulg1  19020  mulgnegnn  19023  isghmOLD  19155  ghmghmrn  19174  cntrnsg  19283  oppgplusfval  19287  pgrpsubgsymg  19346  psgneldm2i  19442  efgrelexlemb  19687  frgp0  19697  frgpmhm  19702  vrgpf  19705  cntrcmnd  19779  cntrabl  19780  cygctb  19829  dprd0  19970  dprd2da  19981  mgpplusg  20060  opprmulfval  20255  subrngint  20476  subrgint  20511  lsp0  20922  rlmval2  21106  cncrng  21307  cnfld1  21312  zringcyg  21386  mulgrhm2  21395  zlmsca  21437  fermltlchr  21446  chrnzr  21447  zrhpsgnelbas  21510  ocvz  21594  cssincl  21604  css0  21605  css1  21606  frlmip  21694  fczpsrbag  21837  ply1idvr1OLD  22189  evls1rhmlem  22215  evl1fval1lem  22224  marrepeval  22457  decpmatid  22664  0opn  22798  topopn  22800  basdif0  22847  tgval  22849  isopn2  22926  0cld  22932  ntropn  22943  ntrval2  22945  ntrdif  22946  clsdif  22947  cmclsopn  22956  ntrtop  22964  ntr0  22975  mretopd  22986  neips  23007  neiptopnei  23026  maxlp  23041  isperf2  23046  rest0  23063  iocpnfordt  23109  icomnfordt  23110  mnfnei  23115  refref  23407  unisngl  23421  1stckgen  23448  ptbasfi  23475  pthaus  23532  fbssfi  23731  isfil2  23750  ssfg  23766  filconn  23777  fbasrn  23778  filufint  23814  imaelfm  23845  fmfnfmlem4  23851  fclsfnflim  23921  alexsubALTlem3  23943  alexsubALTlem4  23944  ustfilxp  24107  ustuqtop2  24137  ustuqtop4  24139  utopsnneiplem  24142  utopsnnei  24144  utop2nei  24145  cfiluweak  24189  neipcfilu  24190  xmetres  24259  metres  24260  mopnex  24414  prdsms  24426  metucn  24466  tngds  24543  tngngp3  24551  nmoge0  24616  cnfldnm  24673  tgioo  24691  xrtgioo  24702  xrsmopn  24708  negcncf  24822  negcncfOLD  24823  phtpy01  24891  pco0  24921  tcphtopn  25133  tchnmfval  25135  caussi  25204  rrxip  25297  minveclem3b  25335  ovolfioo  25375  ovolficc  25376  ovolfsf  25379  ovolctb  25398  ovolctb2  25400  ovolfiniun  25409  ovoliun2  25414  ovolshftlem1  25417  ovolscalem1  25421  ovolicopnf  25432  iunmbl2  25465  uniioombllem2  25491  opnmblALT  25511  ismbf  25536  mbfinf  25573  0plef  25580  itg1climres  25622  itg2cnlem1  25669  iblitg  25676  ibl0  25695  itgcn  25753  cnlimc  25796  dvfre  25862  dvnfre  25863  dveflem  25890  dvef  25891  dvlipcn  25906  lhop2  25927  itgsubstlem  25962  deg1val  26008  ply1rem  26078  coefv0  26160  plyrecj  26194  vieta1lem2  26226  aannenlem1  26243  aaliou2b  26256  ulmval  26296  ulmpm  26299  ulmdvlem1  26316  mtest  26320  efcn  26360  sin2pim  26401  cos2pim  26402  sinmpi  26403  cosmpi  26404  sinppi  26405  cosppi  26406  efimpi  26407  sincosq1lem  26413  sincosq2sgn  26415  sincosq3sgn  26416  sincosq4sgn  26417  sinq12gt0  26423  sinq34lt0t  26425  sincosq1eq  26428  abssinper  26437  efif1o  26462  loglt1b  26550  relogcn  26554  ellogdm  26555  efopn  26574  cxp0  26586  cxp1  26587  cxpsqrt  26619  logsqrt  26620  logb1  26686  atandm3  26795  atanbnd  26843  atancn  26853  leibpi  26859  efrlim  26886  efrlimOLD  26887  logdifbnd  26911  vmaprm  27034  ppip1le  27078  ppieq0  27093  prmorcht  27095  ppiublem1  27120  ppiub  27122  chpeq0  27126  chtub  27130  fsumvma  27131  pclogsum  27133  chpval2  27136  dchrresb  27177  dchrptlem1  27182  lgs0  27228  lgs2  27232  lgsdir2lem2  27244  lgsdir2lem4  27246  lgsdchrval  27272  lgsdchr  27273  lgseisenlem2  27294  2lgslem1c  27311  2lgsoddprmlem2  27327  addsq2nreurex  27362  dirith2  27446  selberg2lem  27468  qabvle  27543  qabvexp  27544  ostth  27557  noextendseq  27586  noetasuplem4  27655  noetainflem4  27659  scutun12  27729  madebdayim  27806  addsrid  27878  addsfo  27897  peano2no  27898  negscl  27949  subsfo  27976  subsid1  27979  muls01  28022  mulsrid  28023  divs1  28114  recsex  28128  abssnid  28152  peano2ons  28183  noseqp1  28192  noseqind  28193  peano2nns  28249  n0sfincut  28253  dfnns2  28268  elzs2  28294  elnnzs  28296  elznns  28297  n0seo  28314  exps0  28320  exps1  28321  istrkg2ld  28394  istrkg3ld  28395  ttgval  28809  brbtwn  28833  colinearalglem4  28843  upgr0eop  29048  uspgrushgr  29111  usgruspgr  29114  usgr0eop  29180  0grsubgr  29212  uspgrloopvtx  29450  umgr2v2evtx  29456  usgr0edg0rusgr  29510  rgrusgrprc  29524  wlkvtxiedg  29560  pthdivtx  29664  usgr2pthlem  29700  wlkswwlksf1o  29816  wwlksext2clwwlk  29993  konigsbergssiedgw  30186  frgrncvvdeqlem7  30241  2clwwlk2  30284  ex-po  30371  pliguhgr  30422  nvnd  30624  ipval2lem3  30641  ipval2  30643  ipidsq  30646  dipcj  30650  dip0r  30653  nmlnogt0  30733  blocni  30741  ipasslem2  30768  ipasslem8  30773  ipasslem9  30774  ajval  30797  ubthlem1  30806  hvaddlid  30959  hvsub0  31012  hi02  31033  hlimi  31124  isch2  31159  chlimi  31170  chsupunss  31280  shsupunss  31282  chlejb1i  31412  h1dei  31486  h1de2ci  31492  spanunsni  31515  pjoml2i  31521  pjorthi  31605  mayete3i  31664  hosubid1  31734  nmopge0  31847  nmfnge0  31863  adj1  31869  adjeq  31871  lnop0  31902  lnopmi  31936  nmophmi  31967  cnlnadjlem5  32007  cnlnadjeui  32013  unierri  32040  leoprf2  32063  leopnmid  32074  nmopleid  32075  hstles  32167  hst0  32169  strlem3a  32188  dmdbr2  32239  mdsl1i  32257  mdsl2i  32258  mdsl2bi  32259  cvmdi  32260  mdslmd1lem1  32261  mdslmd1lem2  32262  mdslmd1i  32265  mdslmd2i  32266  csmdsymi  32270  mdexchi  32271  superpos  32290  atomli  32318  atordi  32320  chirredlem1  32326  chirredlem2  32327  atcvat4i  32333  atabsi  32337  mdsymlem1  32339  mdsymlem5  32343  mdsymlem6  32344  sumdmdii  32351  dmdbr5ati  32358  dmdbr6ati  32359  mddmdin0i  32367  cdj3lem2  32371  unidifsnel  32471  unidifsnne  32472  xppreima  32576  abfmpunirn  32583  abfmpel  32586  aciunf1lem  32593  fgreu  32603  imafi2  32642  padct  32650  fpwrelmapffslem  32662  fpwrelmap  32663  xrge0infss  32690  xrdifh  32710  pfx1s2  32867  clatp0cl  32909  clatp1cl  32910  cntrcrng  33017  cycpmco2lem4  33093  rmfsupp2  33196  1fldgenq  33279  resvval  33308  rearchi  33324  qusxpid  33341  opprabs  33460  zringfrac  33532  rlmdim  33612  constrfiss  33748  2sqr3minply  33777  locfinreflem  33837  locfinref  33838  ordtconnlem1  33921  rge0scvg  33946  lmxrge0  33949  qqh0  33981  qqh1  33982  rrh0  34012  zrhre  34016  esumcst  34060  esumfzf  34066  esumfsupre  34068  hasheuni  34082  sgon  34121  dmvlsiga  34126  sigainb  34133  measval  34195  ismeas  34196  sxbrsigalem0  34269  omssubadd  34298  carsggect  34316  eulerpartlemmf  34373  eulerpartlemgs2  34378  eulerpartlemn  34379  rrvsum  34452  ballotlem2  34487  ballotlemfcc  34492  ballotlem4  34497  signsplypnf  34548  signsply0  34549  signsw0glem  34551  signswrid  34556  signlem0  34585  signshf  34586  bnj535  34887  bnj580  34910  bnj907  34964  bnj1253  35014  funen1cnv  35085  onvf1odlem1  35097  onvf1od  35101  loop1cycl  35131  ptpconn  35227  cvmsss2  35268  cvmlift2lem12  35308  cvmlift2lem13  35309  cvmliftphtlem  35311  cvmliftpht  35312  fmlafvel  35379  mppsthm  35573  bcneg1  35730  fv1stcnv  35771  fv2ndcnv  35772  wlimeq1  35815  imagesset  35948  altopeq1  35958  brcolinear2  36053  cldbnd  36321  ivthALT  36330  refssfne  36353  ontgval  36426  onint1  36444  axc11n11r  36678  bj-pm11.53a  36773  bj-bm1.3ii  37059  bj-restsn0  37080  bj-restsn10  37081  bj-restsnid  37082  bj-rest10  37083  bj-rest0  37088  bj-inftyexpiinv  37203  bj-inftyexpidisj  37205  taupilem1  37316  irrdiff  37321  f1omptsnlem  37331  mptsnunlem  37333  topdifinffinlem  37342  inunissunidif  37370  rdgssun  37373  exrecfnlem  37374  exrecfnpw  37376  finixpnum  37606  tan2h  37613  matunitlindflem2  37618  ptrest  37620  poimirlem22  37643  poimirlem25  37646  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnclem  37672  itg2addnclem2  37673  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  ftc1anclem5  37698  ftc1anclem8  37701  dvasin  37705  dvacos  37706  sdclem2  37743  totbndbnd  37790  heibor1lem  37810  heiborlem7  37818  bfplem1  37823  prnc  38068  brxrn  38363  riotasv  38959  glbconN  39377  glbconNOLD  39378  atpointN  39744  polsubN  39908  pol0N  39910  pol1N  39911  2polvalN  39915  2polssN  39916  3polN  39917  pcl0N  39923  2pmaplubN  39927  pnonsingN  39934  polsubclN  39953  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdleme41sn3a  40434  cdleme32a  40442  cdleme40m  40468  cdleme40n  40469  cdleme42b  40479  istendo  40761  cdlemk40  40918  cdlemkid  40937  dihvalcqpre  41236  facp2  42138  relt0neg1  42451  sn-nnne0  42455  frlmsnic  42535  prjspnerlem  42612  prjspnval2  42613  0prjspn  42623  3cubes  42685  mapfzcons1cl  42713  eldioph3b  42760  eldiophss  42769  0dioph  42773  vdioph  42774  eldioph4b  42806  eldioph4i  42807  rencldnfilem  42815  rmxy1  42918  rmxy0  42919  rmxm1  42930  rmym1  42931  monotoddzzfi  42938  wepwso  43039  aomclem6  43055  pwslnmlem0  43087  isnumbasabl  43102  areaquad  43212  onexlimgt  43239  oaabsb  43290  nadd1suc  43388  om2  43400  oe2  43402  safesnsupfidom1o  43413  onno  43429  oa1cl  43443  finona1cl  43449  reabsifneg  43628  reabsifnneg  43631  relexp2  43673  eltrclrec  43676  elrtrclrec  43677  brtrclrec  43692  brrtrclrec  43693  relexpxpmin  43713  dftrcl3  43716  dfrtrcl3  43729  heeq1  43773  seff  44305  lhe4.4ex1a  44325  eelT0  44771  snssl  44826  sineq0ALT  44933  trfr  44959  xpwf  44961  dmwf  44962  rnwf  44963  modelaxreplem1  44975  modelaxreplem3  44977  0elaxnul  44980  prclaxpr  44982  uniclaxun  44983  wfac8prim  44999  permaxinf2lem  45009  elrnmpt1sf  45190  founiiun0  45191  supxrgere  45336  supxrgelem  45340  fmuldfeqlem1  45587  fmuldfeq  45588  climneg  45615  sumnnodd  45635  liminfltlem  45809  xlimpnfxnegmnf2  45863  addccncf2  45881  dvsinax  45918  stoweidlem18  46023  stoweidlem19  46024  stoweidlem22  46027  stoweidlem34  46039  stoweidlem40  46045  stoweidlem41  46046  stoweidlem55  46060  stoweidlem59  46064  dirker2re  46097  dirkerdenne0  46098  fourierdlem48  46159  fourierdlem49  46160  fourierdlem70  46181  fourierdlem71  46182  fourierdlem104  46215  fourierdlem112  46223  fouriersw  46236  etransclem46  46285  etransclem48  46287  nnfoctbdjlem  46460  ormklocald  46879  natlocalincr  46881  singoutnword  46887  sqrtnegnre  47312  fsummmodsnunz  47380  flsqrt5  47599  bits0ALTV  47684  mogoldbblem  47725  sgoldbeven3prm  47788  nnsum3primes4  47793  isubgr0uhgr  47877  ushggricedg  47931  2zrngnmlid  48247  2zrngnmrid  48248  mpoexxg2  48330  lco0  48420  zlmodzxzldeplem3  48495  0dig1  48602  naryfvalel  48623  ackvalsuc0val  48680  iinxp  48823  0funclem  49079  aacllem  49794