Theorem mpan2 688

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 684	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpanr12  702  mp3an23  1452  elvd  3440  eueq2  3646  sbcgf  3794  sbcralg  3808  csbconstgf  3851  sbcnestgw  4355  csbnestgw  4356  sbcnestg  4360  csbnestg  4361  csbnest1g  4364  mpteq1OLD  5169  iinexg  5266  eusv2nf  5319  reusv2lem5  5326  nnullss  5378  xpss1  5609  xpiindi  5747  reldm0  5840  elrnmpt1s  5869  resdm  5939  eliniseg  6005  trinxp  6035  ssrnres  6086  cnveq0  6105  coi2  6171  relrelss  6180  cnviin  6193  elpred  6223  ord0eln0  6324  funcnvres  6519  funimaex  6529  fnresin1  6566  fnresin2  6567  fresin  6652  ssimaex  6862  fvmpt  6884  fvmptnf  6906  fvimacnvALT  6943  dff3  6985  fsn  7016  fsn2  7017  funop  7030  fvrnressn  7042  fninfp  7055  fndifnfp  7057  fnnfpeq0  7059  fprb  7078  elabrex  7125  f1elima  7145  f1ofvswap  7187  fliftel1  7190  f1owe  7233  sorpssuni  7594  sorpssint  7595  eldifpw  7627  ordeleqon  7641  ordsson  7642  ssnlim  7741  abrexexg  7812  tposfun  8067  tpostpos2  8072  fpr3g  8110  wfr3g  8147  wfrlem14OLD  8162  wfrlem15OLD  8163  tfrlem10  8227  tfrlem12  8229  tfr3  8239  seqomlem1  8290  seqomlem2  8291  seqomlem4  8293  ondif2  8341  oa0  8355  om0  8356  oa1suc  8370  om1  8382  oe1  8384  oe1m  8385  omass  8420  oeoalem  8436  oeoelem  8438  nnmsucr  8465  nnm1  8491  nnm2  8492  ecelqsg  8570  xpider  8586  mapdm0  8639  fvdiagfn  8688  ixpsnf1o  8735  xp1en  8853  undom  8855  sbthlem7  8885  domunsn  8923  xpmapenlem  8940  infensuc  8951  findcard2d  8958  diffi  8971  cnvfi  8972  enreffi  8978  snnen2o  9035  infi  9052  finresfin  9054  unblem1  9075  unblem2  9076  unblem3  9077  unblem4  9078  isfinite2  9081  infn0  9085  unfilem1  9087  unfilem2  9088  unfir  9091  fofinf1o  9103  cnvfiALT  9110  pwfilemOLD  9122  mptfi  9127  finsschain  9135  marypha2  9207  inf0  9388  trcl  9495  frr3g  9523  r1rankidb  9571  snwf  9576  unwf  9577  uniwf  9586  rankval3b  9593  rankr1a  9603  rankxplim3  9648  scott0  9653  djueq1  9672  card1  9735  pm54.43  9768  infxpenc2  9787  dfac8clem  9797  alephsuc2  9845  alephle  9853  cardaleph  9854  dfac12lem2  9909  undjudom  9932  djudom1  9947  pwdju1  9955  nnadju  9962  ackbij1lem18  10002  cflem  10011  cflecard  10018  cfeq0  10021  cfslb  10031  cfsmolem  10035  cfcoflem  10037  cfidm  10040  isfin4p1  10080  fin23lem12  10096  fin23lem16  10100  fin23lem28  10105  fin23lem38  10114  fin23lem41  10117  fin1a2lem7  10171  fin1a2lem12  10176  fin1a2lem13  10177  hsmexlem8  10189  axcc2lem  10201  axcc3  10203  domtriomlem  10207  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  axcclem  10222  ac6num  10244  ttukeylem4  10277  ttukeylem7  10280  ttukey2g  10281  axdclem  10284  brdom3  10293  brdom5  10294  cardeq0  10317  unsnen  10318  konigthlem  10333  pwcfsdom  10348  canthp1lem1  10417  wunex2  10503  wuncval2  10512  eltsk2g  10516  ingru  10580  grutsk  10587  axgroth6  10593  mulidpi  10651  nlt1pi  10671  indpi  10672  pinq  10692  mulidnq  10728  1idpr  10794  prlem934  10798  0idsr  10862  1idsr  10863  00sr  10864  negexsr  10867  recexsrlem  10868  sqgt0sr  10871  ax1rid  10926  axcnre  10929  ne0gt0  11089  peano2cn  11156  peano2re  11157  00id  11159  mul02lem2  11161  mul01  11163  subid  11249  subid1  11250  negid  11277  negeq0  11284  peano2cnm  11296  peano2rem  11297  lt0neg1  11490  le0neg1  11492  relin01  11508  div2neg  11707  recgt0ii  11890  divgt0i2i  11899  ledivp1i  11909  ltdivp1i  11910  peano5nni  11985  peano2nn  11994  nnge1  12010  times2  12119  addltmul  12218  nn0p1nn  12281  peano2nn0  12282  nn0lele2xi  12297  frnnn0supp  12298  frnnn0fsupp  12299  frnnn0suppg  12300  peano2z  12370  peano2zm  12372  suprzcl  12409  zeo  12415  uzwo  12660  uzwo2  12661  infssuzle  12680  infssuzcl  12681  zq  12703  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  rphalfcl  12766  zgt1rpn0n1  12780  ltpnf  12865  nltmnf  12874  pnfge  12875  nltpnft  12907  xlemnf  12910  qsqueeze  12944  xlt0neg1  12962  xle0neg1  12964  xaddpnf1  12969  xaddmnf1  12971  xaddid1  12984  xsubge0  13004  xmul01  13010  xmulneg1  13012  xmulpnf1  13017  xmulid1  13022  supxrbnd  13071  supxrgtmnf  13072  supxrre1  13073  supxrre2  13074  elioopnf  13184  elicopnf  13186  iccshftri  13228  iccshftli  13230  iccdili  13232  icccntri  13234  fzprval  13326  fz0add1fz1  13466  fzofzp1  13493  fzostep1  13512  injresinj  13517  flge0nn0  13549  flge1nn  13550  btwnzge0  13557  modfrac  13613  om2uzsuci  13677  axdc4uzlem  13712  ser1const  13788  exp0  13795  exp1  13797  expn1  13801  nn0sqcl  13819  sqval  13844  sqeq0  13849  resqcl  13853  zsqcl  13857  expubnd  13904  binom21  13943  expnbnd  13956  nn0opthlem2  13992  bcnn  14035  bcn2  14042  bcn2p1  14048  bcnm1  14050  hasheq0  14087  hashsng  14093  hashen1  14094  hashunsnggt  14118  hashin  14135  hashdif  14137  hashgt23el  14148  hashxplem  14157  hashf1lem2  14179  hash2pr  14192  hash2prde  14193  pr2pwpr  14202  hash3tr  14213  iswrd  14228  wrdval  14229  hashwrdn  14259  ccatval2  14292  ccatrid  14301  eqs1  14326  s111  14329  ccatws1len  14334  repsw0  14499  repsw1  14505  cshw0  14516  wwlktovf  14680  relexpsucnnl  14750  reim0  14838  imval2  14871  cjne0  14883  abssq  15027  max0add  15031  abs2dif  15053  rddif  15061  absrdbnd  15062  rexuz3  15069  isershft  15384  isercolllem2  15386  isercoll  15388  fsum  15441  fsumadd  15461  fsumsplitsnun  15476  bcxmas  15556  infcvgaux2i  15579  fprod  15660  risefac0  15746  fallfac0  15747  risefac1  15752  fallfac1  15753  bpoly2  15776  bpoly3  15777  bpoly4  15778  fsumcube  15779  efi4p  15855  resin4p  15856  recos4p  15857  sinbnd  15898  cosbnd  15899  rpnnen2lem8  15939  rpnnen2lem12  15943  cnso  15965  dvdsmul2  15997  dvdslelem  16027  odd2np1lem  16058  mod2eq1n2dvds  16065  divalglem0  16111  divalglem1  16112  divalglem4  16114  divalglem5  16115  divalglem8  16118  flodddiv4  16131  bits0  16144  bitsp1o  16149  bitsf1  16162  sadadd2lem2  16166  gcd1  16244  gcdmultipleOLD  16269  lcm0val  16308  dvdslcm  16312  lcmeq0  16314  lcmgcd  16321  lcm1  16324  lcmfunsnlem2lem2  16353  lcmfunsnlem2  16354  prm2orodd  16405  phiprm  16487  pc0  16564  pcdvdstr  16586  vdwlem2  16692  vdwlem6  16696  vdwlem8  16698  hashbc0  16715  setsval  16877  fsets  16879  setsres  16888  ressinbas  16964  ressress  16967  elrestr  17148  pwssnf1o  17218  xpsfrnel  17282  xpscf  17285  ismred2  17321  submre  17323  mreacs  17376  oppchomfval  17432  oppchomfvalOLD  17433  brssc  17535  isssc  17541  yonedalem4c  18004  oduleval  18016  isprs  18024  oduclatb  18234  gsumval2a  18378  smndex1n0mnd  18560  mulg1  18720  mulgnegnn  18723  isghm  18843  ghmghmrn  18862  cntrnsg  18957  oppgplusfval  18961  pgrpsubgsymg  19026  psgneldm2i  19122  efgrelexlemb  19365  frgp0  19375  frgpmhm  19380  vrgpf  19383  cntrcmnd  19452  cntrabl  19453  cygctb  19502  dprd0  19643  dprd2da  19654  mgpplusg  19733  opprmulfval  19873  subrgint  20055  lsp0  20280  sralemOLD  20449  rlmval2  20473  zringcyg  20700  mulgrhm2  20709  zlmsca  20735  chrnzr  20743  zrhpsgnelbas  20808  ocvz  20892  cssincl  20902  css0  20903  css1  20904  frlmip  20994  fczpsrbag  21135  ply1idvr1  21473  evls1rhmlem  21496  evl1fval1lem  21505  marrepeval  21721  decpmatid  21928  0opn  22062  topopn  22064  basdif0  22112  tgval  22114  isopn2  22192  0cld  22198  ntropn  22209  ntrval2  22211  ntrdif  22212  clsdif  22213  cmclsopn  22222  ntrtop  22230  ntr0  22241  mretopd  22252  neips  22273  neiptopnei  22292  maxlp  22307  isperf2  22312  rest0  22329  iocpnfordt  22375  icomnfordt  22376  mnfnei  22381  refref  22673  unisngl  22687  1stckgen  22714  ptbasfi  22741  pthaus  22798  fbssfi  22997  isfil2  23016  ssfg  23032  filconn  23043  fbasrn  23044  filufint  23080  imaelfm  23111  fmfnfmlem4  23117  fclsfnflim  23187  alexsubALTlem3  23209  alexsubALTlem4  23210  ustfilxp  23373  ustuqtop2  23403  ustuqtop4  23405  utopsnneiplem  23408  utopsnnei  23410  utop2nei  23411  cfiluweak  23456  neipcfilu  23457  xmetres  23526  metres  23527  mopnex  23684  prdsms  23696  metucn  23736  tngds  23820  tngdsOLD  23821  tngngp3  23829  nmoge0  23894  cnfldnm  23951  tgioo  23968  xrtgioo  23978  xrsmopn  23984  negcncf  24094  phtpy01  24157  pco0  24186  tcphtopn  24399  tchnmfval  24401  caussi  24470  rrxip  24563  minveclem3b  24601  ovolfioo  24640  ovolficc  24641  ovolfsf  24644  ovolctb  24663  ovolctb2  24665  ovolfiniun  24674  ovoliun2  24679  ovolshftlem1  24682  ovolscalem1  24686  ovolicopnf  24697  iunmbl2  24730  uniioombllem2  24756  opnmblALT  24776  ismbf  24801  mbfinf  24838  0plef  24845  itg1climres  24888  itg2cnlem1  24935  iblitg  24942  ibl0  24960  itgcn  25018  cnlimc  25061  dvfre  25124  dvnfre  25125  dveflem  25152  dvef  25153  dvlipcn  25167  lhop2  25188  itgsubstlem  25221  deg1val  25270  ply1rem  25337  coefv0  25418  plyrecj  25449  vieta1lem2  25480  aannenlem1  25497  aaliou2b  25510  ulmval  25548  ulmpm  25551  ulmdvlem1  25568  mtest  25572  efcn  25611  sin2pim  25651  cos2pim  25652  sinmpi  25653  cosmpi  25654  sinppi  25655  cosppi  25656  efimpi  25657  sincosq1lem  25663  sincosq2sgn  25665  sincosq3sgn  25666  sincosq4sgn  25667  sinq12gt0  25673  sinq34lt0t  25675  sincosq1eq  25678  abssinper  25686  efif1o  25711  loglt1b  25798  relogcn  25802  ellogdm  25803  efopn  25822  cxp0  25834  cxp1  25835  cxpsqrt  25867  logsqrt  25868  logb1  25928  atandm3  26037  atanbnd  26085  atancn  26095  leibpi  26101  efrlim  26128  logdifbnd  26152  vmaprm  26275  ppip1le  26319  ppieq0  26334  prmorcht  26336  ppiublem1  26359  ppiub  26361  chpeq0  26365  chtub  26369  fsumvma  26370  pclogsum  26372  chpval2  26375  dchrresb  26416  dchrptlem1  26421  lgs0  26467  lgs2  26471  lgsdir2lem2  26483  lgsdir2lem4  26485  lgsdchrval  26511  lgsdchr  26512  lgseisenlem2  26533  2lgslem1c  26550  2lgsoddprmlem2  26566  addsq2nreurex  26601  dirith2  26685  selberg2lem  26707  qabvle  26782  qabvexp  26783  ostth  26796  istrkg2ld  26830  istrkg3ld  26831  ttgval  27245  ttgvalOLD  27246  cchhllemOLD  27264  brbtwn  27276  colinearalglem4  27286  upgr0eop  27493  uspgrushgr  27554  usgruspgr  27557  usgr0eop  27622  0grsubgr  27654  uspgrloopvtx  27891  umgr2v2evtx  27897  usgr0edg0rusgr  27951  rgrusgrprc  27965  wlkvtxiedg  28001  pthdivtx  28106  usgr2pthlem  28140  wlkswwlksf1o  28253  wwlksext2clwwlk  28430  konigsbergssiedgw  28623  frgrncvvdeqlem7  28678  2clwwlk2  28721  ex-po  28808  pliguhgr  28857  nvnd  29059  ipval2lem3  29076  ipval2  29078  ipidsq  29081  dipcj  29085  dip0r  29088  nmlnogt0  29168  blocni  29176  ipasslem2  29203  ipasslem8  29208  ipasslem9  29209  ajval  29232  ubthlem1  29241  hvaddid2  29394  hvsub0  29447  hi02  29468  hlimi  29559  isch2  29594  chlimi  29605  chsupunss  29715  shsupunss  29717  chlejb1i  29847  h1dei  29921  h1de2ci  29927  spanunsni  29950  pjoml2i  29956  pjorthi  30040  mayete3i  30099  hosubid1  30169  nmopge0  30282  nmfnge0  30298  adj1  30304  adjeq  30306  lnop0  30337  lnopmi  30371  nmophmi  30402  cnlnadjlem5  30442  cnlnadjeui  30448  unierri  30475  leoprf2  30498  leopnmid  30509  nmopleid  30510  hstles  30602  hst0  30604  strlem3a  30623  dmdbr2  30674  mdsl1i  30692  mdsl2i  30693  mdsl2bi  30694  cvmdi  30695  mdslmd1lem1  30696  mdslmd1lem2  30697  mdslmd1i  30700  mdslmd2i  30701  csmdsymi  30705  mdexchi  30706  superpos  30725  atomli  30753  atordi  30755  chirredlem1  30761  chirredlem2  30762  atcvat4i  30768  atabsi  30772  mdsymlem1  30774  mdsymlem5  30778  mdsymlem6  30779  sumdmdii  30786  dmdbr5ati  30793  dmdbr6ati  30794  mddmdin0i  30802  cdj3lem2  30806  unidifsnel  30892  unidifsnne  30893  xppreima  30992  abfmpunirn  30998  abfmpel  31001  aciunf1lem  31008  fgreu  31018  imafi2  31055  padct  31063  fpwrelmapffslem  31076  fpwrelmap  31077  xrge0infss  31092  xrdifh  31110  pfx1s2  31222  clatp0cl  31263  clatp1cl  31264  cntrcrng  31331  cycpmco2lem4  31405  rmfsupp2  31501  resvval  31535  rearchi  31555  qusxpid  31568  locfinreflem  31799  locfinref  31800  ordtconnlem1  31883  rge0scvg  31908  lmxrge0  31911  qqh0  31943  qqh1  31944  rrh0  31974  zrhre  31978  esumcst  32040  esumfzf  32046  esumfsupre  32048  hasheuni  32062  sgon  32101  dmvlsiga  32106  sigainb  32113  measval  32175  ismeas  32176  sxbrsigalem0  32247  omssubadd  32276  carsggect  32294  eulerpartlemmf  32351  eulerpartlemgs2  32356  eulerpartlemn  32357  rrvsum  32430  ballotlem2  32464  ballotlemfcc  32469  ballotlem4  32474  signsplypnf  32538  signsply0  32539  signsw0glem  32541  signswrid  32546  signlem0  32575  signshf  32576  bnj535  32879  bnj580  32902  bnj907  32956  bnj1253  33006  funen1cnv  33069  loop1cycl  33108  ptpconn  33204  cvmsss2  33245  cvmlift2lem12  33285  cvmlift2lem13  33286  cvmliftphtlem  33288  cvmliftpht  33289  fmlafvel  33356  mppsthm  33550  onelssex  33670  bcneg1  33711  fv1stcnv  33760  fv2ndcnv  33761  wlimeq1  33823  naddid1  33845  noextendseq  33879  noetasuplem4  33948  noetainflem4  33952  scutun12  34013  madebdayim  34079  addsid1  34136  imagesset  34264  altopeq1  34274  brcolinear2  34369  cldbnd  34524  ivthALT  34533  refssfne  34556  ontgval  34629  onint1  34647  axc11n11r  34874  bj-pm11.53a  34969  bj-bm1.3ii  35244  bj-restsn0  35265  bj-restsn10  35266  bj-restsnid  35267  bj-rest10  35268  bj-rest0  35273  bj-inftyexpiinv  35388  bj-inftyexpidisj  35390  taupilem1  35501  irrdiff  35506  f1omptsnlem  35516  mptsnunlem  35518  topdifinffinlem  35527  inunissunidif  35555  rdgssun  35558  exrecfnlem  35559  exrecfnpw  35561  finixpnum  35771  tan2h  35778  matunitlindflem2  35783  ptrest  35785  poimirlem22  35808  poimirlem25  35811  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  itg2addnclem  35837  itg2addnclem2  35838  itg2addnclem3  35839  itg2addnc  35840  itg2gt0cn  35841  ftc1anclem5  35863  ftc1anclem8  35866  dvasin  35870  dvacos  35871  sdclem2  35909  totbndbnd  35956  heibor1lem  35976  heiborlem7  35984  bfplem1  35989  prnc  36234  ecexALTV  36473  brxrn  36511  riotasv  36980  glbconN  37398  atpointN  37764  polsubN  37928  pol0N  37930  pol1N  37931  2polvalN  37935  2polssN  37936  3polN  37937  pcl0N  37943  2pmaplubN  37947  pnonsingN  37954  polsubclN  37973  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme41sn3a  38454  cdleme32a  38462  cdleme40m  38488  cdleme40n  38489  cdleme42b  38499  istendo  38781  cdlemk40  38938  cdlemkid  38957  dihvalcqpre  39256  facp2  40106  fac2xp3  40167  2xp3dxp2ge1d  40169  factwoffsmonot  40170  fnsnbt  40215  frlmsnic  40270  relt0neg1  40432  sn-inelr  40442  prjspnerlem  40463  prjspnval2  40464  0prjspn  40472  3cubes  40519  mapfzcons1cl  40547  eldioph3b  40594  eldiophss  40603  0dioph  40607  vdioph  40608  eldioph4b  40640  eldioph4i  40641  rencldnfilem  40649  rmxy1  40751  rmxy0  40752  rmxm1  40763  rmym1  40764  monotoddzzfi  40771  wepwso  40875  aomclem6  40891  pwslnmlem0  40923  isnumbasabl  40938  areaquad  41054  oa1cl  41061  finona1cl  41067  reabsifneg  41247  reabsifnneg  41250  relexp2  41292  eltrclrec  41295  elrtrclrec  41296  brtrclrec  41311  brrtrclrec  41312  relexpxpmin  41332  dftrcl3  41335  dfrtrcl3  41348  heeq1  41392  seff  41934  lhe4.4ex1a  41954  eelT0  42402  snssl  42457  sineq0ALT  42564  elabrexg  42596  elrnmpt1sf  42734  founiiun0  42735  supxrgere  42879  supxrgelem  42883  fmuldfeqlem1  43130  fmuldfeq  43131  climneg  43158  sumnnodd  43178  liminfltlem  43352  xlimpnfxnegmnf2  43406  addccncf2  43424  dvsinax  43461  stoweidlem18  43566  stoweidlem19  43567  stoweidlem22  43570  stoweidlem34  43582  stoweidlem40  43588  stoweidlem41  43589  stoweidlem55  43603  stoweidlem59  43607  dirker2re  43640  dirkerdenne0  43641  fourierdlem48  43702  fourierdlem49  43703  fourierdlem70  43724  fourierdlem71  43725  fourierdlem104  43758  fourierdlem112  43766  fouriersw  43779  etransclem46  43828  etransclem48  43830  nnfoctbdjlem  44000  sqrtnegnre  44810  fsummmodsnunz  44838  flsqrt5  45057  bits0ALTV  45142  mogoldbblem  45183  sgoldbeven3prm  45246  nnsum3primes4  45251  ushrisomgr  45304  2zrngnmlid  45518  2zrngnmrid  45519  mpoexxg2  45684  lco0  45779  zlmodzxzldeplem3  45854  0dig1  45966  naryfvalel  45987  ackvalsuc0val  46044  aacllem  46516  natlocalincr  46522  singoutnword  46528