Theorem mpan2 690

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  mpanr12  704  mp3an23  1450  elvd  3447  eueq2  3649  sbcgf  3791  sbcralg  3803  csbconstgf  3846  csb0  4314  sbcnestgw  4328  csbnestgw  4329  sbcnestg  4333  csbnestg  4334  csbnest1g  4337  mpteq1  5118  iinexg  5208  eusv2nf  5261  reusv2lem5  5268  nnullss  5319  xpss1  5538  xpiindi  5670  reldm0  5762  elrnmpt1s  5793  resdm  5863  eliniseg  5925  trinxp  5952  ssrnres  6002  cnveq0  6021  coi2  6083  relrelss  6092  cnviin  6105  ord0eln0  6213  funcnvres  6402  funimaex  6411  fnresin1  6444  fnresin2  6445  fresin  6521  ssimaex  6723  fvmpt  6745  fvmptnf  6767  fvimacnvALT  6804  dff3  6843  fsn  6874  fsn2  6875  funop  6888  fvrnressn  6900  fninfp  6913  fndifnfp  6915  fnnfpeq0  6917  fprb  6933  elabrex  6980  f1elima  6999  fliftel1  7042  f1owe  7085  sorpssuni  7438  sorpssint  7439  eldifpw  7470  ordeleqon  7483  ordsson  7484  ssnlim  7579  tposfun  7891  tpostpos2  7896  wfr3g  7936  wfrlem14  7951  wfrlem15  7952  tfrlem10  8006  tfrlem12  8008  tfr3  8018  seqomlem1  8069  seqomlem2  8070  seqomlem4  8072  ondif2  8110  oa0  8124  om0  8125  oa1suc  8139  om1  8151  oe1  8153  oe1m  8154  omass  8189  oeoalem  8205  oeoelem  8207  nnmsucr  8234  nnm1  8258  nnm2  8259  ecelqsg  8335  xpider  8351  mapdm0  8404  fvdiagfn  8438  ixpsnf1o  8485  xp1en  8586  sbthlem7  8617  domunsn  8651  xpmapenlem  8668  infensuc  8679  infi  8726  finresfin  8728  diffi  8734  findcard2d  8744  unblem1  8754  unblem2  8755  unblem3  8756  unblem4  8757  isfinite2  8760  infn0  8764  unfilem1  8766  unfilem2  8767  unfir  8770  fofinf1o  8783  cnvfi  8790  pwfilem  8802  mptfi  8807  finsschain  8815  marypha2  8887  inf0  9068  trcl  9154  r1rankidb  9217  snwf  9222  unwf  9223  uniwf  9232  rankval3b  9239  rankr1a  9249  rankxplim3  9294  scott0  9299  djueq1  9318  card1  9381  pm54.43  9414  infxpenc2  9433  dfac8clem  9443  alephsuc2  9491  alephle  9499  cardaleph  9500  dfac12lem2  9555  undjudom  9578  djudom1  9593  pwdju1  9601  nnadju  9608  ackbij1lem18  9648  cflem  9657  cflecard  9664  cfeq0  9667  cfslb  9677  cfsmolem  9681  cfcoflem  9683  cfidm  9686  isfin4p1  9726  fin23lem12  9742  fin23lem16  9746  fin23lem28  9751  fin23lem38  9760  fin23lem41  9763  fin1a2lem7  9817  fin1a2lem12  9822  fin1a2lem13  9823  hsmexlem8  9835  axcc2lem  9847  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  axcclem  9868  ac6num  9890  ttukeylem4  9923  ttukeylem7  9926  ttukey2g  9927  axdclem  9930  brdom3  9939  brdom5  9940  cardeq0  9963  unsnen  9964  konigthlem  9979  pwcfsdom  9994  canthp1lem1  10063  wunex2  10149  wuncval2  10158  eltsk2g  10162  ingru  10226  grutsk  10233  axgroth6  10239  mulidpi  10297  nlt1pi  10317  indpi  10318  pinq  10338  mulidnq  10374  1idpr  10440  prlem934  10444  0idsr  10508  1idsr  10509  00sr  10510  negexsr  10513  recexsrlem  10514  sqgt0sr  10517  ax1rid  10572  axcnre  10575  ne0gt0  10734  peano2cn  10801  peano2re  10802  00id  10804  mul02lem2  10806  mul01  10808  subid  10894  subid1  10895  negid  10922  negeq0  10929  peano2cnm  10941  peano2rem  10942  lt0neg1  11135  le0neg1  11137  relin01  11153  div2neg  11352  recgt0ii  11535  divgt0i2i  11544  ledivp1i  11554  ltdivp1i  11555  peano5nni  11628  peano2nn  11637  nnge1  11653  times2  11762  addltmul  11861  nn0p1nn  11924  peano2nn0  11925  nn0lele2xi  11940  frnnn0fsupp  11942  peano2z  12011  peano2zm  12013  suprzcl  12050  zeo  12056  uzwo  12299  uzwo2  12300  infssuzle  12319  infssuzcl  12320  zq  12342  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  rphalfcl  12404  zgt1rpn0n1  12418  ltpnf  12503  nltmnf  12512  pnfge  12513  nltpnft  12545  xlemnf  12548  qsqueeze  12582  xlt0neg1  12600  xle0neg1  12602  xaddpnf1  12607  xaddmnf1  12609  xaddid1  12622  xsubge0  12642  xmul01  12648  xmulneg1  12650  xmulpnf1  12655  xmulid1  12660  supxrbnd  12709  supxrgtmnf  12710  supxrre1  12711  supxrre2  12712  elioopnf  12821  elicopnf  12823  iccshftri  12865  iccshftli  12867  iccdili  12869  icccntri  12871  fzprval  12963  fz0add1fz1  13102  fzofzp1  13129  fzostep1  13148  injresinj  13153  flge0nn0  13185  flge1nn  13186  btwnzge0  13193  modfrac  13247  om2uzsuci  13311  axdc4uzlem  13346  ser1const  13422  exp0  13429  exp1  13431  expn1  13435  nn0sqcl  13452  sqval  13477  sqeq0  13482  resqcl  13486  zsqcl  13490  expubnd  13537  binom21  13576  expnbnd  13589  nn0opthlem2  13625  bcnn  13668  bcn2  13675  bcn2p1  13681  bcnm1  13683  hasheq0  13720  hashsng  13726  hashen1  13727  hashunsnggt  13751  hashin  13768  hashdif  13770  hashgt23el  13781  hashxplem  13790  hashf1lem2  13810  hash2pr  13823  hash2prde  13824  pr2pwpr  13833  hash3tr  13844  iswrd  13859  wrdval  13860  hashwrdn  13890  ccatval2  13923  ccatrid  13932  eqs1  13957  s111  13960  ccatws1len  13965  repsw0  14130  repsw1  14136  cshw0  14147  wwlktovf  14311  relexpsucnnl  14381  reim0  14469  imval2  14502  cjne0  14514  abssq  14658  max0add  14662  abs2dif  14684  rddif  14692  absrdbnd  14693  rexuz3  14700  isershft  15012  isercolllem2  15014  isercoll  15016  fsum  15069  fsumadd  15088  fsumsplitsnun  15102  bcxmas  15182  infcvgaux2i  15205  fprod  15287  risefac0  15373  fallfac0  15374  risefac1  15379  fallfac1  15380  bpoly2  15403  bpoly3  15404  bpoly4  15405  fsumcube  15406  efi4p  15482  resin4p  15483  recos4p  15484  sinbnd  15525  cosbnd  15526  rpnnen2lem8  15566  rpnnen2lem12  15570  cnso  15592  dvdsmul2  15624  dvdslelem  15651  odd2np1lem  15681  mod2eq1n2dvds  15688  divalglem0  15734  divalglem1  15735  divalglem4  15737  divalglem5  15738  divalglem8  15741  flodddiv4  15754  bits0  15767  bitsp1o  15772  bitsf1  15785  sadadd2lem2  15789  gcd1  15866  gcdmultipleOLD  15890  lcm0val  15928  dvdslcm  15932  lcmeq0  15934  lcmgcd  15941  lcm1  15944  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  prm2orodd  16025  phiprm  16104  pc0  16181  pcdvdstr  16202  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  hashbc0  16331  setsval  16505  fsets  16508  setsres  16517  ressinbas  16552  ressress  16554  elrestr  16694  pwssnf1o  16763  xpsfrnel  16827  xpscf  16830  ismred2  16866  submre  16868  mreacs  16921  oppchomfval  16976  brssc  17076  isssc  17082  yonedalem4c  17519  isprs  17532  oduleval  17733  oduclatb  17746  gsumval2a  17887  smndex1n0mnd  18069  mulg1  18227  mulgnegnn  18230  isghm  18350  ghmghmrn  18369  cntrnsg  18464  oppgplusfval  18468  pgrpsubgsymg  18529  psgneldm2i  18625  efgrelexlemb  18868  frgp0  18878  frgpmhm  18883  vrgpf  18886  cntrcmnd  18955  cntrabl  18956  cygctb  19005  dprd0  19146  dprd2da  19157  mgpplusg  19236  opprmulfval  19371  subrgint  19550  lsp0  19774  sralem  19942  rlmval2  19959  zringcyg  20184  mulgrhm2  20192  zlmsca  20214  chrnzr  20222  zrhpsgnelbas  20283  ocvz  20367  cssincl  20377  css0  20378  css1  20379  frlmip  20467  fczpsrbag  20605  ply1idvr1  20922  evls1rhmlem  20945  evl1fval1lem  20954  marrepeval  21168  decpmatid  21375  0opn  21509  topopn  21511  basdif0  21558  tgval  21560  isopn2  21637  0cld  21643  ntropn  21654  ntrval2  21656  ntrdif  21657  clsdif  21658  cmclsopn  21667  ntrtop  21675  ntr0  21686  mretopd  21697  neips  21718  neiptopnei  21737  maxlp  21752  isperf2  21757  rest0  21774  iocpnfordt  21820  icomnfordt  21821  mnfnei  21826  refref  22118  unisngl  22132  1stckgen  22159  ptbasfi  22186  pthaus  22243  fbssfi  22442  isfil2  22461  ssfg  22477  filconn  22488  fbasrn  22489  filufint  22525  imaelfm  22556  fmfnfmlem4  22562  fclsfnflim  22632  alexsubALTlem3  22654  alexsubALTlem4  22655  ustfilxp  22818  ustuqtop2  22848  ustuqtop4  22850  utopsnneiplem  22853  utopsnnei  22855  utop2nei  22856  cfiluweak  22901  neipcfilu  22902  xmetres  22971  metres  22972  mopnex  23126  prdsms  23138  metucn  23178  tngds  23254  tngngp3  23262  nmoge0  23327  cnfldnm  23384  tgioo  23401  xrtgioo  23411  xrsmopn  23417  negcncf  23527  phtpy01  23590  pco0  23619  tcphtopn  23830  tchnmfval  23832  caussi  23901  rrxip  23994  minveclem3b  24032  ovolfioo  24071  ovolficc  24072  ovolfsf  24075  ovolctb  24094  ovolctb2  24096  ovolfiniun  24105  ovoliun2  24110  ovolshftlem1  24113  ovolscalem1  24117  ovolicopnf  24128  iunmbl2  24161  uniioombllem2  24187  opnmblALT  24207  ismbf  24232  mbfinf  24269  0plef  24276  itg1climres  24318  itg2cnlem1  24365  iblitg  24372  ibl0  24390  itgcn  24448  cnlimc  24491  dvfre  24554  dvnfre  24555  dveflem  24582  dvef  24583  dvlipcn  24597  lhop2  24618  itgsubstlem  24651  deg1val  24697  ply1rem  24764  coefv0  24845  plyrecj  24876  vieta1lem2  24907  aannenlem1  24924  aaliou2b  24937  ulmval  24975  ulmpm  24978  ulmdvlem1  24995  mtest  24999  efcn  25038  sin2pim  25078  cos2pim  25079  sinmpi  25080  cosmpi  25081  sinppi  25082  cosppi  25083  efimpi  25084  sincosq1lem  25090  sincosq2sgn  25092  sincosq3sgn  25093  sincosq4sgn  25094  sinq12gt0  25100  sinq34lt0t  25102  sincosq1eq  25105  abssinper  25113  efif1o  25138  loglt1b  25225  relogcn  25229  ellogdm  25230  efopn  25249  cxp0  25261  cxp1  25262  cxpsqrt  25294  logsqrt  25295  logb1  25355  atandm3  25464  atanbnd  25512  atancn  25522  leibpi  25528  efrlim  25555  logdifbnd  25579  vmaprm  25702  ppip1le  25746  ppieq0  25761  prmorcht  25763  ppiublem1  25786  ppiub  25788  chpeq0  25792  chtub  25796  fsumvma  25797  pclogsum  25799  chpval2  25802  dchrresb  25843  dchrptlem1  25848  lgs0  25894  lgs2  25898  lgsdir2lem2  25910  lgsdir2lem4  25912  lgsdchrval  25938  lgsdchr  25939  lgseisenlem2  25960  2lgslem1c  25977  2lgsoddprmlem2  25993  addsq2nreurex  26028  dirith2  26112  selberg2lem  26134  qabvle  26209  qabvexp  26210  ostth  26223  istrkg2ld  26254  istrkg3ld  26255  ttgval  26669  cchhllem  26681  brbtwn  26693  colinearalglem4  26703  upgr0eop  26907  uspgrushgr  26968  usgruspgr  26971  usgr0eop  27036  0grsubgr  27068  uspgrloopvtx  27305  umgr2v2evtx  27311  usgr0edg0rusgr  27365  rgrusgrprc  27379  wlkvtxiedg  27414  pthdivtx  27518  usgr2pthlem  27552  wlkswwlksf1o  27665  wwlksext2clwwlk  27842  konigsbergssiedgw  28035  frgrncvvdeqlem7  28090  2clwwlk2  28133  ex-po  28220  pliguhgr  28269  nvnd  28471  ipval2lem3  28488  ipval2  28490  ipidsq  28493  dipcj  28497  dip0r  28500  nmlnogt0  28580  blocni  28588  ipasslem2  28615  ipasslem8  28620  ipasslem9  28621  ajval  28644  ubthlem1  28653  hvaddid2  28806  hvsub0  28859  hi02  28880  hlimi  28971  isch2  29006  chlimi  29017  chsupunss  29127  shsupunss  29129  chlejb1i  29259  h1dei  29333  h1de2ci  29339  spanunsni  29362  pjoml2i  29368  pjorthi  29452  mayete3i  29511  hosubid1  29581  nmopge0  29694  nmfnge0  29710  adj1  29716  adjeq  29718  lnop0  29749  lnopmi  29783  nmophmi  29814  cnlnadjlem5  29854  cnlnadjeui  29860  unierri  29887  leoprf2  29910  leopnmid  29921  nmopleid  29922  hstles  30014  hst0  30016  strlem3a  30035  dmdbr2  30086  mdsl1i  30104  mdsl2i  30105  mdsl2bi  30106  cvmdi  30107  mdslmd1lem1  30108  mdslmd1lem2  30109  mdslmd1i  30112  mdslmd2i  30113  csmdsymi  30117  mdexchi  30118  superpos  30137  atomli  30165  atordi  30167  chirredlem1  30173  chirredlem2  30174  atcvat4i  30180  atabsi  30184  mdsymlem1  30186  mdsymlem5  30190  mdsymlem6  30191  sumdmdii  30198  dmdbr5ati  30205  dmdbr6ati  30206  mddmdin0i  30214  cdj3lem2  30218  unidifsnel  30307  unidifsnne  30308  xppreima  30408  abfmpunirn  30415  abfmpel  30418  aciunf1lem  30425  fgreu  30435  imafi2  30473  padct  30481  fpwrelmapffslem  30494  fpwrelmap  30495  xrge0infss  30510  xrdifh  30529  pfx1s2  30641  clatp0cl  30684  clatp1cl  30685  cntrcrng  30747  cycpmco2lem4  30821  rmfsupp2  30917  resvval  30951  rearchi  30966  qusxpid  30979  locfinreflem  31193  locfinref  31194  ordtconnlem1  31277  rge0scvg  31302  lmxrge0  31305  qqh0  31335  qqh1  31336  rrh0  31366  zrhre  31370  esumcst  31432  esumfzf  31438  esumfsupre  31440  hasheuni  31454  sgon  31493  dmvlsiga  31498  sigainb  31505  measval  31567  ismeas  31568  sxbrsigalem0  31639  omssubadd  31668  carsggect  31686  eulerpartlemmf  31743  eulerpartlemgs2  31748  eulerpartlemn  31749  rrvsum  31822  ballotlem2  31856  ballotlemfcc  31861  ballotlem4  31866  signsplypnf  31930  signsply0  31931  signsw0glem  31933  signswrid  31938  signlem0  31967  signshf  31968  bnj535  32272  bnj580  32295  bnj907  32349  bnj1253  32399  funen1cnv  32467  loop1cycl  32497  ptpconn  32593  cvmsss2  32634  cvmlift2lem12  32674  cvmlift2lem13  32675  cvmliftphtlem  32677  cvmliftpht  32678  fmlafvel  32745  mppsthm  32939  bcneg1  33081  fv1stcnv  33133  fv2ndcnv  33134  trpred0  33188  wlimeq1  33220  frr3g  33234  fpr3g  33235  noextendseq  33287  noetalem3  33332  scutun12  33384  imagesset  33527  altopeq1  33537  brcolinear2  33632  cldbnd  33787  ivthALT  33796  refssfne  33819  ontgval  33892  onint1  33910  axc11n11r  34130  bj-bm1.3ii  34481  bj-restsn0  34500  bj-restsn10  34501  bj-restsnid  34502  bj-rest10  34503  bj-rest0  34508  bj-inftyexpiinv  34623  bj-inftyexpidisj  34625  taupilem1  34735  irrdiff  34740  f1omptsnlem  34753  mptsnunlem  34755  topdifinffinlem  34764  inunissunidif  34792  rdgssun  34795  exrecfnlem  34796  exrecfnpw  34798  finixpnum  35042  tan2h  35049  matunitlindflem2  35054  ptrest  35056  poimirlem22  35079  poimirlem25  35082  mblfinlem1  35094  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  itg2addnclem  35108  itg2addnclem2  35109  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  ftc1anclem5  35134  ftc1anclem8  35137  dvasin  35141  dvacos  35142  sdclem2  35180  totbndbnd  35227  heibor1lem  35247  heiborlem7  35255  bfplem1  35260  prnc  35505  ecexALTV  35748  brxrn  35786  riotasv  36255  glbconN  36673  atpointN  37039  polsubN  37203  pol0N  37205  pol1N  37206  2polvalN  37210  2polssN  37211  3polN  37212  pcl0N  37218  2pmaplubN  37222  pnonsingN  37229  polsubclN  37248  cdlemefs32sn1aw  37710  cdleme43fsv1snlem  37716  cdleme41sn3a  37729  cdleme32a  37737  cdleme40m  37763  cdleme40n  37764  cdleme42b  37774  istendo  38056  cdlemk40  38213  cdlemkid  38232  dihvalcqpre  38531  facp2  39347  fac2xp3  39385  2xp3dxp2ge1d  39387  factwoffsmonot  39388  fnsnbt  39414  frlmsnic  39453  relt0neg1  39580  sn-inelr  39590  0prjspn  39614  3cubes  39631  mapfzcons1cl  39659  eldioph3b  39706  eldiophss  39715  0dioph  39719  vdioph  39720  eldioph4b  39752  eldioph4i  39753  rencldnfilem  39761  rmxy1  39863  rmxy0  39864  rmxm1  39875  rmym1  39876  monotoddzzfi  39883  aomclem6  40003  pwslnmlem0  40035  isnumbasabl  40050  areaquad  40166  reabsifneg  40332  reabsifnneg  40335  relexp2  40378  eltrclrec  40381  elrtrclrec  40382  brtrclrec  40397  brrtrclrec  40398  relexpxpmin  40418  dftrcl3  40421  dfrtrcl3  40434  heeq1  40478  seff  41013  lhe4.4ex1a  41033  eelT0  41481  snssl  41536  sineq0ALT  41643  elabrexg  41675  elrnmpt1sf  41816  founiiun0  41817  supxrgere  41965  supxrgelem  41969  fmuldfeqlem1  42224  fmuldfeq  42225  climneg  42252  sumnnodd  42272  liminfltlem  42446  xlimpnfxnegmnf2  42500  addccncf2  42518  dvsinax  42555  stoweidlem18  42660  stoweidlem19  42661  stoweidlem22  42664  stoweidlem34  42676  stoweidlem40  42682  stoweidlem41  42683  stoweidlem55  42697  stoweidlem59  42701  dirker2re  42734  dirkerdenne0  42735  fourierdlem48  42796  fourierdlem49  42797  fourierdlem70  42818  fourierdlem71  42819  fourierdlem104  42852  fourierdlem112  42860  fouriersw  42873  etransclem46  42922  etransclem48  42924  nnfoctbdjlem  43094  sqrtnegnre  43864  fsummmodsnunz  43892  flsqrt5  44111  bits0ALTV  44197  mogoldbblem  44238  sgoldbeven3prm  44301  nnsum3primes4  44306  ushrisomgr  44359  2zrngnmlid  44573  2zrngnmrid  44574  mpoexxg2  44739  lco0  44836  zlmodzxzldeplem3  44911  0dig1  45023  naryfvalel  45044  ackvalsuc0val  45101  aacllem  45329