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  1452  elvd  3483  eueq2  3718  sbcgf  3867  sbcralg  3882  csbconstgf  3925  sbcnestgw  4428  csbnestgw  4429  sbcnestg  4433  csbnestg  4434  csbnest1g  4437  mpteq1OLD  5241  iinexg  5353  eusv2nf  5400  reusv2lem5  5407  nnullss  5472  xpss1  5707  xpiindi  5848  reldm0  5940  elrnmpt1s  5972  resdm  6045  eliniseg  6114  trinxp  6147  ssrnres  6199  cnveq0  6218  coi2  6284  relrelss  6294  cnviin  6307  elpred  6339  onelssex  6433  ord0eln0  6440  funcnvres  6645  funimaex  6655  fnresin1  6693  fnresin2  6694  fresin  6777  ssimaex  6993  fvmpt  7015  fvmptnf  7037  fvimacnvALT  7076  dff3  7119  fsn  7154  fsn2  7155  funop  7168  fvrnressn  7180  fninfp  7193  fndifnfp  7195  fnnfpeq0  7197  fprb  7213  elabrex  7261  elabrexg  7262  f1elima  7282  f1ofvswap  7325  fliftel1  7329  f1owe  7372  sorpssuni  7750  sorpssint  7751  eldifpw  7786  ordeleqon  7800  ordsson  7801  ssnlim  7906  abrexexg  7983  tposfun  8265  tpostpos2  8270  fpr3g  8308  wfr3g  8345  wfrlem14OLD  8360  wfrlem15OLD  8361  tfrlem10  8425  tfrlem12  8427  tfr3  8437  seqomlem1  8488  seqomlem2  8489  seqomlem4  8491  ondif2  8538  oa0  8552  om0  8553  oa1suc  8567  om1  8578  oe1  8580  oe1m  8581  omass  8616  oeoalem  8632  oeoelem  8634  nnmsucr  8661  nnm1  8688  nnm2  8689  naddrid  8719  naddlid  8720  ecelqsg  8810  xpider  8826  mapdm0  8880  fvdiagfn  8929  ixpsnf1o  8976  xp1en  9095  undom  9097  sbthlem7  9127  domunsn  9165  xpmapenlem  9182  infensuc  9193  findcard2d  9204  diffi  9213  cnvfi  9214  enreffi  9220  snnen2o  9270  1sdom2dom  9280  infi  9299  finresfin  9301  unblem1  9325  unblem2  9326  unblem3  9327  unblem4  9328  isfinite2  9331  infn0ALT  9338  unfilem1  9340  unfilem2  9341  unfir  9343  fofinf1o  9369  cnvfiALT  9376  mptfi  9388  finsschain  9396  marypha2  9476  inf0  9658  trcl  9765  frr3g  9793  r1rankidb  9841  snwf  9846  unwf  9847  uniwf  9856  rankval3b  9863  rankr1a  9873  rankxplim3  9918  scott0  9923  djueq1  9942  card1  10005  pm54.43  10038  infxpenc2  10059  dfac8clem  10069  alephsuc2  10117  alephle  10125  cardaleph  10126  dfac12lem2  10182  undjudom  10205  djudom1  10220  pwdju1  10228  nnadju  10235  ackbij1lem18  10273  cflem  10282  cflemOLD  10283  cflecard  10290  cfeq0  10293  cfslb  10303  cfsmolem  10307  cfcoflem  10309  cfidm  10312  isfin4p1  10352  fin23lem12  10368  fin23lem16  10372  fin23lem28  10377  fin23lem38  10386  fin23lem41  10389  fin1a2lem7  10443  fin1a2lem12  10448  fin1a2lem13  10449  hsmexlem8  10461  axcc2lem  10473  axcc3  10475  domtriomlem  10479  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  ac6num  10516  ttukeylem4  10549  ttukeylem7  10552  ttukey2g  10553  axdclem  10556  brdom3  10565  brdom5  10566  cardeq0  10589  unsnen  10590  konigthlem  10605  pwcfsdom  10620  canthp1lem1  10689  wunex2  10775  wuncval2  10784  eltsk2g  10788  ingru  10852  grutsk  10859  axgroth6  10865  mulidpi  10923  nlt1pi  10943  indpi  10944  pinq  10964  mulidnq  11000  1idpr  11066  prlem934  11070  0idsr  11134  1idsr  11135  00sr  11136  negexsr  11139  recexsrlem  11140  sqgt0sr  11143  ax1rid  11198  axcnre  11201  ne0gt0  11363  peano2cn  11430  peano2re  11431  00id  11433  mul02lem2  11435  mul01  11437  subid  11525  subid1  11526  negid  11553  negeq0  11560  peano2cnm  11572  peano2rem  11573  lt0neg1  11766  le0neg1  11768  relin01  11784  div2neg  11987  recgt0ii  12171  divgt0i2i  12180  ledivp1i  12190  ltdivp1i  12191  peano5nni  12266  peano2nn  12275  nnge1  12291  nnne0  12297  times2  12400  addltmul  12499  nn0p1nn  12562  peano2nn0  12563  nn0lele2xi  12579  fcdmnn0supp  12580  fcdmnn0fsupp  12581  fcdmnn0suppg  12582  peano2z  12655  peano2zm  12657  suprzcl  12695  zeo  12701  eluzaddi  12906  uzwo  12950  uzwo2  12951  infssuzle  12970  infssuzcl  12971  zq  12993  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  rphalfcl  13059  zgt1rpn0n1  13073  ltpnf  13159  nltmnf  13168  pnfge  13169  nltpnft  13202  xlemnf  13205  qsqueeze  13239  xlt0neg1  13257  xle0neg1  13259  xaddpnf1  13264  xaddmnf1  13266  xaddrid  13279  xsubge0  13299  xmul01  13305  xmulneg1  13307  xmulpnf1  13312  xmulrid  13317  supxrbnd  13366  supxrgtmnf  13367  supxrre1  13368  supxrre2  13369  elioopnf  13479  elicopnf  13481  iccshftri  13523  iccshftli  13525  iccdili  13527  icccntri  13529  fzprval  13621  fz0add1fz1  13770  fzofzp1  13799  fzostep1  13818  injresinj  13823  flge0nn0  13856  flge1nn  13857  btwnzge0  13864  modfrac  13920  om2uzsuci  13985  axdc4uzlem  14020  ser1const  14095  exp0  14102  exp1  14104  expn1  14108  nn0sqcl  14126  sqval  14151  sqeq0  14156  resqcl  14160  zsqcl  14165  expubnd  14213  binom21  14254  expnbnd  14267  nn0opthlem2  14304  bcnn  14347  bcn2  14354  bcn2p1  14360  bcnm1  14362  hasheq0  14398  hashsng  14404  hashen1  14405  hashunsnggt  14429  hashin  14446  hashdif  14448  hashgt23el  14459  hashxplem  14468  hashf1lem2  14491  hash2pr  14504  hash2prde  14505  pr2pwpr  14514  hash3tr  14526  iswrd  14550  wrdval  14551  hashwrdn  14581  ccatval2  14612  ccatrid  14621  eqs1  14646  s111  14649  ccatws1len  14654  repsw0  14811  repsw1  14817  cshw0  14828  wwlktovf  14991  relexpsucnnl  15065  reim0  15153  imval2  15186  cjne0  15198  abssq  15341  max0add  15345  abs2dif  15367  rddif  15375  absrdbnd  15376  rexuz3  15383  isershft  15696  isercolllem2  15698  isercoll  15700  fsum  15752  fsumadd  15772  fsumsplitsnun  15787  bcxmas  15867  infcvgaux2i  15890  fprod  15973  risefac0  16059  fallfac0  16060  risefac1  16065  fallfac1  16066  bpoly2  16089  bpoly3  16090  bpoly4  16091  fsumcube  16092  efi4p  16169  resin4p  16170  recos4p  16171  sinbnd  16212  cosbnd  16213  rpnnen2lem8  16253  rpnnen2lem12  16257  cnso  16279  dvdsmul2  16312  dvdslelem  16342  odd2np1lem  16373  mod2eq1n2dvds  16380  divalglem0  16426  divalglem1  16427  divalglem4  16429  divalglem5  16430  divalglem8  16433  flodddiv4  16448  bits0  16461  bitsp1o  16466  bitsf1  16479  sadadd2lem2  16483  gcd1  16561  lcm0val  16627  dvdslcm  16631  lcmeq0  16633  lcmgcd  16640  lcm1  16643  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  prm2orodd  16724  phiprm  16810  pc0  16887  pcdvdstr  16909  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  hashbc0  17038  setsval  17200  fsets  17202  setsres  17211  ressinbas  17290  ressress  17293  elrestr  17474  pwssnf1o  17544  xpsfrnel  17608  xpscf  17611  ismred2  17647  submre  17649  mreacs  17702  oppchomfval  17758  oppchomfvalOLD  17759  brssc  17861  isssc  17867  yonedalem4c  18333  oduleval  18345  isprs  18353  oduclatb  18564  gsumval2a  18710  smndex1n0mnd  18937  mulg1  19111  mulgnegnn  19114  isghmOLD  19246  ghmghmrn  19265  cntrnsg  19374  oppgplusfval  19378  pgrpsubgsymg  19441  psgneldm2i  19537  efgrelexlemb  19782  frgp0  19792  frgpmhm  19797  vrgpf  19800  cntrcmnd  19874  cntrabl  19875  cygctb  19924  dprd0  20065  dprd2da  20076  mgpplusg  20155  opprmulfval  20352  subrngint  20576  subrgint  20611  lsp0  21024  sralemOLD  21193  rlmval2  21216  cncrng  21418  cnfld1  21423  zringcyg  21497  mulgrhm2  21506  zlmsca  21552  fermltlchr  21561  chrnzr  21562  zrhpsgnelbas  21629  ocvz  21713  cssincl  21723  css0  21724  css1  21725  frlmip  21815  fczpsrbag  21958  ply1idvr1OLD  22314  evls1rhmlem  22340  evl1fval1lem  22349  marrepeval  22584  decpmatid  22791  0opn  22925  topopn  22927  basdif0  22975  tgval  22977  isopn2  23055  0cld  23061  ntropn  23072  ntrval2  23074  ntrdif  23075  clsdif  23076  cmclsopn  23085  ntrtop  23093  ntr0  23104  mretopd  23115  neips  23136  neiptopnei  23155  maxlp  23170  isperf2  23175  rest0  23192  iocpnfordt  23238  icomnfordt  23239  mnfnei  23244  refref  23536  unisngl  23550  1stckgen  23577  ptbasfi  23604  pthaus  23661  fbssfi  23860  isfil2  23879  ssfg  23895  filconn  23906  fbasrn  23907  filufint  23943  imaelfm  23974  fmfnfmlem4  23980  fclsfnflim  24050  alexsubALTlem3  24072  alexsubALTlem4  24073  ustfilxp  24236  ustuqtop2  24266  ustuqtop4  24268  utopsnneiplem  24271  utopsnnei  24273  utop2nei  24274  cfiluweak  24319  neipcfilu  24320  xmetres  24389  metres  24390  mopnex  24547  prdsms  24559  metucn  24599  tngds  24683  tngdsOLD  24684  tngngp3  24692  nmoge0  24757  cnfldnm  24814  tgioo  24831  xrtgioo  24841  xrsmopn  24847  negcncf  24961  negcncfOLD  24962  phtpy01  25030  pco0  25060  tcphtopn  25273  tchnmfval  25275  caussi  25344  rrxip  25437  minveclem3b  25475  ovolfioo  25515  ovolficc  25516  ovolfsf  25519  ovolctb  25538  ovolctb2  25540  ovolfiniun  25549  ovoliun2  25554  ovolshftlem1  25557  ovolscalem1  25561  ovolicopnf  25572  iunmbl2  25605  uniioombllem2  25631  opnmblALT  25651  ismbf  25676  mbfinf  25713  0plef  25720  itg1climres  25763  itg2cnlem1  25810  iblitg  25817  ibl0  25836  itgcn  25894  cnlimc  25937  dvfre  26003  dvnfre  26004  dveflem  26031  dvef  26032  dvlipcn  26047  lhop2  26068  itgsubstlem  26103  deg1val  26149  ply1rem  26219  coefv0  26301  plyrecj  26335  vieta1lem2  26367  aannenlem1  26384  aaliou2b  26397  ulmval  26437  ulmpm  26440  ulmdvlem1  26457  mtest  26461  efcn  26501  sin2pim  26541  cos2pim  26542  sinmpi  26543  cosmpi  26544  sinppi  26545  cosppi  26546  efimpi  26547  sincosq1lem  26553  sincosq2sgn  26555  sincosq3sgn  26556  sincosq4sgn  26557  sinq12gt0  26563  sinq34lt0t  26565  sincosq1eq  26568  abssinper  26577  efif1o  26602  loglt1b  26690  relogcn  26694  ellogdm  26695  efopn  26714  cxp0  26726  cxp1  26727  cxpsqrt  26759  logsqrt  26760  logb1  26826  atandm3  26935  atanbnd  26983  atancn  26993  leibpi  26999  efrlim  27026  efrlimOLD  27027  logdifbnd  27051  vmaprm  27174  ppip1le  27218  ppieq0  27233  prmorcht  27235  ppiublem1  27260  ppiub  27262  chpeq0  27266  chtub  27270  fsumvma  27271  pclogsum  27273  chpval2  27276  dchrresb  27317  dchrptlem1  27322  lgs0  27368  lgs2  27372  lgsdir2lem2  27384  lgsdir2lem4  27386  lgsdchrval  27412  lgsdchr  27413  lgseisenlem2  27434  2lgslem1c  27451  2lgsoddprmlem2  27467  addsq2nreurex  27502  dirith2  27586  selberg2lem  27608  qabvle  27683  qabvexp  27684  ostth  27697  noextendseq  27726  noetasuplem4  27795  noetainflem4  27799  scutun12  27869  madebdayim  27940  addsrid  28011  addsfo  28030  peano2no  28031  negscl  28082  subsfo  28109  subsid1  28112  muls01  28152  mulsrid  28153  divs1  28243  recsex  28257  abssnid  28281  peano2ons  28302  noseqp1  28311  noseqind  28312  peano2nns  28367  dfnns2  28376  elzs2  28399  elnnzs  28401  elznns  28402  n0seo  28419  exps0  28424  exps1  28425  istrkg2ld  28482  istrkg3ld  28483  ttgval  28897  ttgvalOLD  28898  cchhllemOLD  28916  brbtwn  28928  colinearalglem4  28938  upgr0eop  29145  uspgrushgr  29208  usgruspgr  29211  usgr0eop  29277  0grsubgr  29309  uspgrloopvtx  29547  umgr2v2evtx  29553  usgr0edg0rusgr  29607  rgrusgrprc  29621  wlkvtxiedg  29657  pthdivtx  29761  usgr2pthlem  29795  wlkswwlksf1o  29908  wwlksext2clwwlk  30085  konigsbergssiedgw  30278  frgrncvvdeqlem7  30333  2clwwlk2  30376  ex-po  30463  pliguhgr  30514  nvnd  30716  ipval2lem3  30733  ipval2  30735  ipidsq  30738  dipcj  30742  dip0r  30745  nmlnogt0  30825  blocni  30833  ipasslem2  30860  ipasslem8  30865  ipasslem9  30866  ajval  30889  ubthlem1  30898  hvaddlid  31051  hvsub0  31104  hi02  31125  hlimi  31216  isch2  31251  chlimi  31262  chsupunss  31372  shsupunss  31374  chlejb1i  31504  h1dei  31578  h1de2ci  31584  spanunsni  31607  pjoml2i  31613  pjorthi  31697  mayete3i  31756  hosubid1  31826  nmopge0  31939  nmfnge0  31955  adj1  31961  adjeq  31963  lnop0  31994  lnopmi  32028  nmophmi  32059  cnlnadjlem5  32099  cnlnadjeui  32105  unierri  32132  leoprf2  32155  leopnmid  32166  nmopleid  32167  hstles  32259  hst0  32261  strlem3a  32280  dmdbr2  32331  mdsl1i  32349  mdsl2i  32350  mdsl2bi  32351  cvmdi  32352  mdslmd1lem1  32353  mdslmd1lem2  32354  mdslmd1i  32357  mdslmd2i  32358  csmdsymi  32362  mdexchi  32363  superpos  32382  atomli  32410  atordi  32412  chirredlem1  32418  chirredlem2  32419  atcvat4i  32425  atabsi  32429  mdsymlem1  32431  mdsymlem5  32435  mdsymlem6  32436  sumdmdii  32443  dmdbr5ati  32450  dmdbr6ati  32451  mddmdin0i  32459  cdj3lem2  32463  unidifsnel  32560  unidifsnne  32561  xppreima  32661  abfmpunirn  32668  abfmpel  32671  aciunf1lem  32678  fgreu  32688  imafi2  32728  padct  32736  fpwrelmapffslem  32749  fpwrelmap  32750  xrge0infss  32770  xrdifh  32788  pfx1s2  32907  clatp0cl  32950  clatp1cl  32951  cntrcrng  33055  cycpmco2lem4  33131  rmfsupp2  33227  1fldgenq  33303  resvval  33332  rearchi  33353  qusxpid  33370  opprabs  33489  zringfrac  33561  rlmdim  33636  2sqr3minply  33752  locfinreflem  33800  locfinref  33801  ordtconnlem1  33884  rge0scvg  33909  lmxrge0  33912  qqh0  33946  qqh1  33947  rrh0  33977  zrhre  33981  esumcst  34043  esumfzf  34049  esumfsupre  34051  hasheuni  34065  sgon  34104  dmvlsiga  34109  sigainb  34116  measval  34178  ismeas  34179  sxbrsigalem0  34252  omssubadd  34281  carsggect  34299  eulerpartlemmf  34356  eulerpartlemgs2  34361  eulerpartlemn  34362  rrvsum  34435  ballotlem2  34469  ballotlemfcc  34474  ballotlem4  34479  signsplypnf  34543  signsply0  34544  signsw0glem  34546  signswrid  34551  signlem0  34580  signshf  34581  bnj535  34882  bnj580  34905  bnj907  34959  bnj1253  35009  funen1cnv  35080  loop1cycl  35121  ptpconn  35217  cvmsss2  35258  cvmlift2lem12  35298  cvmlift2lem13  35299  cvmliftphtlem  35301  cvmliftpht  35302  fmlafvel  35369  mppsthm  35563  bcneg1  35715  fv1stcnv  35757  fv2ndcnv  35758  wlimeq1  35801  imagesset  35934  altopeq1  35944  brcolinear2  36039  cldbnd  36308  ivthALT  36317  refssfne  36340  ontgval  36413  onint1  36431  axc11n11r  36665  bj-pm11.53a  36760  bj-bm1.3ii  37046  bj-restsn0  37067  bj-restsn10  37068  bj-restsnid  37069  bj-rest10  37070  bj-rest0  37075  bj-inftyexpiinv  37190  bj-inftyexpidisj  37192  taupilem1  37303  irrdiff  37308  f1omptsnlem  37318  mptsnunlem  37320  topdifinffinlem  37329  inunissunidif  37357  rdgssun  37360  exrecfnlem  37361  exrecfnpw  37363  finixpnum  37591  tan2h  37598  matunitlindflem2  37603  ptrest  37605  poimirlem22  37628  poimirlem25  37631  mblfinlem1  37643  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnclem  37657  itg2addnclem2  37658  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  ftc1anclem5  37683  ftc1anclem8  37686  dvasin  37690  dvacos  37691  sdclem2  37728  totbndbnd  37775  heibor1lem  37795  heiborlem7  37803  bfplem1  37808  prnc  38053  ecexALTV  38312  brxrn  38355  riotasv  38940  glbconN  39358  glbconNOLD  39359  atpointN  39725  polsubN  39889  pol0N  39891  pol1N  39892  2polvalN  39896  2polssN  39897  3polN  39898  pcl0N  39904  2pmaplubN  39908  pnonsingN  39915  polsubclN  39934  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme41sn3a  40415  cdleme32a  40423  cdleme40m  40449  cdleme40n  40450  cdleme42b  40460  istendo  40742  cdlemk40  40899  cdlemkid  40918  dihvalcqpre  41217  facp2  42124  fac2xp3  42220  2xp3dxp2ge1d  42222  factwoffsmonot  42223  fnsnbt  42249  relt0neg1  42450  sn-nnne0  42454  sn-inelr  42473  frlmsnic  42526  prjspnerlem  42603  prjspnval2  42604  0prjspn  42614  3cubes  42677  mapfzcons1cl  42705  eldioph3b  42752  eldiophss  42761  0dioph  42765  vdioph  42766  eldioph4b  42798  eldioph4i  42799  rencldnfilem  42807  rmxy1  42910  rmxy0  42911  rmxm1  42922  rmym1  42923  monotoddzzfi  42930  wepwso  43031  aomclem6  43047  pwslnmlem0  43079  isnumbasabl  43094  areaquad  43204  onexlimgt  43231  oaabsb  43283  nadd1suc  43381  om2  43393  oe2  43395  safesnsupfidom1o  43406  onno  43422  oa1cl  43436  finona1cl  43442  reabsifneg  43621  reabsifnneg  43624  relexp2  43666  eltrclrec  43669  elrtrclrec  43670  brtrclrec  43685  brrtrclrec  43686  relexpxpmin  43706  dftrcl3  43709  dfrtrcl3  43722  heeq1  43766  seff  44304  lhe4.4ex1a  44324  eelT0  44772  snssl  44827  sineq0ALT  44934  xpwf  44938  dmwf  44939  rnwf  44940  modelaxreplem1  44942  modelaxreplem3  44944  prclaxpr  44947  elrnmpt1sf  45131  founiiun0  45132  supxrgere  45282  supxrgelem  45286  fmuldfeqlem1  45537  fmuldfeq  45538  climneg  45565  sumnnodd  45585  liminfltlem  45759  xlimpnfxnegmnf2  45813  addccncf2  45831  dvsinax  45868  stoweidlem18  45973  stoweidlem19  45974  stoweidlem22  45977  stoweidlem34  45989  stoweidlem40  45995  stoweidlem41  45996  stoweidlem55  46010  stoweidlem59  46014  dirker2re  46047  dirkerdenne0  46048  fourierdlem48  46109  fourierdlem49  46110  fourierdlem70  46131  fourierdlem71  46132  fourierdlem104  46165  fourierdlem112  46173  fouriersw  46186  etransclem46  46235  etransclem48  46237  nnfoctbdjlem  46410  natlocalincr  46829  singoutnword  46835  upwrdfi  46840  sqrtnegnre  47256  fsummmodsnunz  47299  flsqrt5  47518  bits0ALTV  47603  mogoldbblem  47644  sgoldbeven3prm  47707  nnsum3primes4  47712  isubgr0uhgr  47796  ushggricedg  47833  2zrngnmlid  48098  2zrngnmrid  48099  mpoexxg2  48182  lco0  48272  zlmodzxzldeplem3  48347  0dig1  48458  naryfvalel  48479  ackvalsuc0val  48536  aacllem  49031