Theorem mpan2 689

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanr12  703  mp3an23  1449  elvd  3500  eueq2  3701  sbcgf  3845  sbcralg  3857  csbconstgf  3901  sbcnestgw  4372  csbnestgw  4373  sbcnestg  4377  csbnestg  4378  csbnest1g  4381  mpteq1  5154  iinexg  5244  eusv2nf  5296  reusv2lem5  5303  nnullss  5354  xpss1  5574  xpiindi  5706  reldm0  5798  elrnmpt1s  5829  resdm  5897  eliniseg  5958  trinxp  5985  ssrnres  6035  cnveq0  6054  coi2  6116  relrelss  6124  cnviin  6137  ord0eln0  6245  funcnvres  6432  funimaex  6441  fnresin1  6472  fnresin2  6473  fresin  6547  ssimaex  6748  fvmpt  6768  fvmptnf  6790  fvimacnvALT  6827  dff3  6866  fsn  6897  fsn2  6898  funop  6911  fvrnressn  6923  fninfp  6936  fndifnfp  6938  fnnfpeq0  6940  fprb  6956  elabrex  7002  f1elima  7021  fliftel1  7063  f1owe  7106  sorpssuni  7458  sorpssint  7459  eldifpw  7490  ordeleqon  7503  ordsson  7504  ssnlim  7599  tposfun  7908  tpostpos2  7913  wfr3g  7953  wfrlem14  7968  wfrlem15  7969  tfrlem10  8023  tfrlem12  8025  tfr3  8035  seqomlem1  8086  seqomlem2  8087  seqomlem4  8089  ondif2  8127  oa0  8141  om0  8142  oa1suc  8156  om1  8168  oe1  8170  oe1m  8171  omass  8206  oeoalem  8222  oeoelem  8224  nnmsucr  8251  nnm1  8275  nnm2  8276  ecelqsg  8352  xpider  8368  mapdm0  8421  fvdiagfn  8455  ixpsnf1o  8502  xp1en  8603  sbthlem7  8633  domunsn  8667  xpmapenlem  8684  infensuc  8695  infi  8742  finresfin  8744  diffi  8750  findcard2d  8760  unblem1  8770  unblem2  8771  unblem3  8772  unblem4  8773  isfinite2  8776  infn0  8780  unfilem1  8782  unfilem2  8783  unfir  8786  fofinf1o  8799  cnvfi  8806  pwfilem  8818  mptfi  8823  finsschain  8831  marypha2  8903  inf0  9084  trcl  9170  r1rankidb  9233  snwf  9238  unwf  9239  uniwf  9248  rankval3b  9255  rankr1a  9265  rankxplim3  9310  scott0  9315  djueq1  9334  card1  9397  pm54.43  9429  infxpenc2  9448  dfac8clem  9458  alephsuc2  9506  alephle  9514  cardaleph  9515  dfac12lem2  9570  undjudom  9593  djudom1  9608  pwdju1  9616  ackbij1lem18  9659  cflem  9668  cflecard  9675  cfeq0  9678  cfslb  9688  cfsmolem  9692  cfcoflem  9694  cfidm  9697  isfin4p1  9737  fin23lem12  9753  fin23lem16  9757  fin23lem28  9762  fin23lem38  9771  fin23lem41  9774  fin1a2lem7  9828  fin1a2lem12  9833  fin1a2lem13  9834  hsmexlem8  9846  axcc2lem  9858  axcc3  9860  domtriomlem  9864  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  axcclem  9879  ac6num  9901  ttukeylem4  9934  ttukeylem7  9937  ttukey2g  9938  axdclem  9941  brdom3  9950  brdom5  9951  cardeq0  9974  unsnen  9975  konigthlem  9990  pwcfsdom  10005  canthp1lem1  10074  wunex2  10160  wuncval2  10169  eltsk2g  10173  ingru  10237  grutsk  10244  axgroth6  10250  mulidpi  10308  nlt1pi  10328  indpi  10329  pinq  10349  mulidnq  10385  1idpr  10451  prlem934  10455  0idsr  10519  1idsr  10520  00sr  10521  negexsr  10524  recexsrlem  10525  sqgt0sr  10528  ax1rid  10583  axcnre  10586  ne0gt0  10745  peano2cn  10812  peano2re  10813  00id  10815  mul02lem2  10817  mul01  10819  subid  10905  subid1  10906  negid  10933  negeq0  10940  peano2cnm  10952  peano2rem  10953  lt0neg1  11146  le0neg1  11148  relin01  11164  div2neg  11363  recgt0ii  11546  divgt0i2i  11555  ledivp1i  11565  ltdivp1i  11566  peano5nni  11641  peano2nn  11650  nnge1  11666  times2  11775  addltmul  11874  nn0p1nn  11937  peano2nn0  11938  nn0lele2xi  11953  frnnn0fsupp  11955  peano2z  12024  peano2zm  12026  suprzcl  12063  zeo  12069  uzwo  12312  uzwo2  12313  infssuzle  12332  infssuzcl  12333  zq  12355  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  rphalfcl  12417  zgt1rpn0n1  12431  ltpnf  12516  nltmnf  12525  pnfge  12526  nltpnft  12558  xlemnf  12561  qsqueeze  12595  xlt0neg1  12613  xle0neg1  12615  xaddpnf1  12620  xaddmnf1  12622  xaddid1  12635  xsubge0  12655  xmul01  12661  xmulneg1  12663  xmulpnf1  12668  xmulid1  12673  supxrbnd  12722  supxrgtmnf  12723  supxrre1  12724  supxrre2  12725  elioopnf  12832  elicopnf  12834  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  fzprval  12969  fz0add1fz1  13108  fzofzp1  13135  fzostep1  13154  injresinj  13159  flge0nn0  13191  flge1nn  13192  btwnzge0  13199  modfrac  13253  om2uzsuci  13317  axdc4uzlem  13352  ser1const  13427  exp0  13434  exp1  13436  expn1  13440  nn0sqcl  13457  sqval  13482  sqeq0  13487  resqcl  13491  zsqcl  13495  expubnd  13542  binom21  13581  expnbnd  13594  nn0opthlem2  13630  bcnn  13673  bcn2  13680  bcn2p1  13686  bcnm1  13688  hasheq0  13725  hashsng  13731  hashen1  13732  hashunsnggt  13756  hashin  13773  hashdif  13775  hashgt23el  13786  hashxplem  13795  hashf1lem2  13815  hash2pr  13828  hash2prde  13829  pr2pwpr  13838  hash3tr  13849  iswrd  13864  wrdval  13865  hashwrdn  13898  ccatval2  13932  ccatrid  13941  eqs1  13966  s111  13969  ccatws1len  13974  repsw0  14139  repsw1  14145  cshw0  14156  wwlktovf  14320  relexpsucnnl  14391  reim0  14477  imval2  14510  cjne0  14522  abssq  14666  max0add  14670  abs2dif  14692  rddif  14700  absrdbnd  14701  rexuz3  14708  isershft  15020  isercolllem2  15022  isercoll  15024  fsum  15077  fsumadd  15096  fsumsplitsnun  15110  bcxmas  15190  infcvgaux2i  15213  fprod  15295  risefac0  15381  fallfac0  15382  risefac1  15387  fallfac1  15388  bpoly2  15411  bpoly3  15412  bpoly4  15413  fsumcube  15414  efi4p  15490  resin4p  15491  recos4p  15492  sinbnd  15533  cosbnd  15534  rpnnen2lem8  15574  rpnnen2lem12  15578  cnso  15600  dvdsmul2  15632  dvdslelem  15659  odd2np1lem  15689  mod2eq1n2dvds  15696  divalglem0  15744  divalglem1  15745  divalglem4  15747  divalglem5  15748  divalglem8  15751  flodddiv4  15764  bits0  15777  bitsp1o  15782  bitsf1  15795  sadadd2lem2  15799  gcd1  15876  gcdmultipleOLD  15900  lcm0val  15938  dvdslcm  15942  lcmeq0  15944  lcmgcd  15951  lcm1  15954  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  prm2orodd  16035  phiprm  16114  pc0  16191  pcdvdstr  16212  vdwlem2  16318  vdwlem6  16322  vdwlem8  16324  hashbc0  16341  setsval  16513  fsets  16516  setsres  16525  ressinbas  16560  ressress  16562  elrestr  16702  pwssnf1o  16771  xpsfrnel  16835  xpscf  16838  ismred2  16874  submre  16876  mreacs  16929  oppchomfval  16984  brssc  17084  isssc  17090  yonedalem4c  17527  isprs  17540  oduleval  17741  oduclatb  17754  gsumval2a  17895  smndex1n0mnd  18077  mulg1  18235  mulgnegnn  18238  isghm  18358  ghmghmrn  18377  cntrnsg  18472  oppgplusfval  18476  pgrpsubgsymg  18537  psgneldm2i  18633  efgrelexlemb  18876  frgp0  18886  frgpmhm  18891  vrgpf  18894  cntrcmnd  18962  cntrabl  18963  cygctb  19012  dprd0  19153  dprd2da  19164  mgpplusg  19243  opprmulfval  19375  subrgint  19557  lsp0  19781  sralem  19949  rlmval2  19966  fczpsrbag  20147  ply1idvr1  20461  evls1rhmlem  20484  evl1fval1lem  20493  zringcyg  20638  mulgrhm2  20646  zlmsca  20668  chrnzr  20677  zrhpsgnelbas  20738  ocvz  20822  cssincl  20832  css0  20833  css1  20834  frlmip  20922  marrepeval  21172  decpmatid  21378  0opn  21512  topopn  21514  basdif0  21561  tgval  21563  isopn2  21640  0cld  21646  ntropn  21657  ntrval2  21659  ntrdif  21660  clsdif  21661  cmclsopn  21670  ntrtop  21678  ntr0  21689  mretopd  21700  neips  21721  neiptopnei  21740  maxlp  21755  isperf2  21760  rest0  21777  iocpnfordt  21823  icomnfordt  21824  mnfnei  21829  refref  22121  unisngl  22135  1stckgen  22162  ptbasfi  22189  pthaus  22246  fbssfi  22445  isfil2  22464  ssfg  22480  filconn  22491  fbasrn  22492  filufint  22528  imaelfm  22559  fmfnfmlem4  22565  fclsfnflim  22635  alexsubALTlem3  22657  alexsubALTlem4  22658  ustfilxp  22821  ustuqtop2  22851  ustuqtop4  22853  utopsnneiplem  22856  utopsnnei  22858  utop2nei  22859  cfiluweak  22904  neipcfilu  22905  xmetres  22974  metres  22975  mopnex  23129  prdsms  23141  metucn  23181  tngds  23257  tngngp3  23265  nmoge0  23330  cnfldnm  23387  tgioo  23404  xrtgioo  23414  xrsmopn  23420  negcncf  23526  phtpy01  23589  pco0  23618  tcphtopn  23829  tchnmfval  23831  caussi  23900  rrxip  23993  minveclem3b  24031  ovolfioo  24068  ovolficc  24069  ovolfsf  24072  ovolctb  24091  ovolctb2  24093  ovolfiniun  24102  ovoliun2  24107  ovolshftlem1  24110  ovolscalem1  24114  ovolicopnf  24125  iunmbl2  24158  uniioombllem2  24184  opnmblALT  24204  ismbf  24229  mbfinf  24266  0plef  24273  itg1climres  24315  itg2cnlem1  24362  iblitg  24369  ibl0  24387  itgcn  24443  cnlimc  24486  dvfre  24548  dvnfre  24549  dveflem  24576  dvef  24577  dvlipcn  24591  lhop2  24612  itgsubstlem  24645  deg1val  24690  ply1rem  24757  coefv0  24838  plyrecj  24869  vieta1lem2  24900  aannenlem1  24917  aaliou2b  24930  ulmval  24968  ulmpm  24971  ulmdvlem1  24988  mtest  24992  efcn  25031  sin2pim  25071  cos2pim  25072  sinmpi  25073  cosmpi  25074  sinppi  25075  cosppi  25076  efimpi  25077  sincosq1lem  25083  sincosq2sgn  25085  sincosq3sgn  25086  sincosq4sgn  25087  sinq12gt0  25093  sinq34lt0t  25095  sincosq1eq  25098  abssinper  25106  efif1o  25130  loglt1b  25217  relogcn  25221  ellogdm  25222  efopn  25241  cxp0  25253  cxp1  25254  cxpsqrt  25286  logsqrt  25287  logb1  25347  atandm3  25456  atanbnd  25504  atancn  25514  leibpi  25520  efrlim  25547  logdifbnd  25571  vmaprm  25694  ppip1le  25738  ppieq0  25753  prmorcht  25755  ppiublem1  25778  ppiub  25780  chpeq0  25784  chtub  25788  fsumvma  25789  pclogsum  25791  chpval2  25794  dchrresb  25835  dchrptlem1  25840  lgs0  25886  lgs2  25890  lgsdir2lem2  25902  lgsdir2lem4  25904  lgsdchrval  25930  lgsdchr  25931  lgseisenlem2  25952  2lgslem1c  25969  2lgsoddprmlem2  25985  addsq2nreurex  26020  dirith2  26104  selberg2lem  26126  qabvle  26201  qabvexp  26202  ostth  26215  istrkg2ld  26246  istrkg3ld  26247  ttgval  26661  cchhllem  26673  brbtwn  26685  colinearalglem4  26695  upgr0eop  26899  uspgrushgr  26960  usgruspgr  26963  usgr0eop  27028  0grsubgr  27060  uspgrloopvtx  27297  umgr2v2evtx  27303  usgr0edg0rusgr  27357  rgrusgrprc  27371  wlkvtxiedg  27406  pthdivtx  27510  usgr2pthlem  27544  wlkswwlksf1o  27657  wwlksext2clwwlk  27836  konigsbergssiedgw  28029  frgrncvvdeqlem7  28084  2clwwlk2  28127  ex-po  28214  pliguhgr  28263  nvnd  28465  ipval2lem3  28482  ipval2  28484  ipidsq  28487  dipcj  28491  dip0r  28494  nmlnogt0  28574  blocni  28582  ipasslem2  28609  ipasslem8  28614  ipasslem9  28615  ajval  28638  ubthlem1  28647  hvaddid2  28800  hvsub0  28853  hi02  28874  hlimi  28965  isch2  29000  chlimi  29011  chsupunss  29121  shsupunss  29123  chlejb1i  29253  h1dei  29327  h1de2ci  29333  spanunsni  29356  pjoml2i  29362  pjorthi  29446  mayete3i  29505  hosubid1  29575  nmopge0  29688  nmfnge0  29704  adj1  29710  adjeq  29712  lnop0  29743  lnopmi  29777  nmophmi  29808  cnlnadjlem5  29848  cnlnadjeui  29854  unierri  29881  leoprf2  29904  leopnmid  29915  nmopleid  29916  hstles  30008  hst0  30010  strlem3a  30029  dmdbr2  30080  mdsl1i  30098  mdsl2i  30099  mdsl2bi  30100  cvmdi  30101  mdslmd1lem1  30102  mdslmd1lem2  30103  mdslmd1i  30106  mdslmd2i  30107  csmdsymi  30111  mdexchi  30112  superpos  30131  atomli  30159  atordi  30161  chirredlem1  30167  chirredlem2  30168  atcvat4i  30174  atabsi  30178  mdsymlem1  30180  mdsymlem5  30184  mdsymlem6  30185  sumdmdii  30192  dmdbr5ati  30199  dmdbr6ati  30200  mddmdin0i  30208  cdj3lem2  30212  unidifsnel  30295  unidifsnne  30296  xppreima  30394  abfmpunirn  30397  abfmpel  30400  aciunf1lem  30407  fgreu  30417  imafi2  30447  padct  30455  fpwrelmapffslem  30468  fpwrelmap  30469  xrge0infss  30484  xrdifh  30503  pfx1s2  30615  clatp0cl  30658  clatp1cl  30659  cntrcrng  30697  cycpmco2lem4  30771  rmfsupp2  30866  resvval  30900  rearchi  30915  qusxpid  30928  locfinreflem  31104  locfinref  31105  ordtconnlem1  31167  rge0scvg  31192  lmxrge0  31195  qqh0  31225  qqh1  31226  rrh0  31256  zrhre  31260  esumcst  31322  esumfzf  31328  esumfsupre  31330  hasheuni  31344  sgon  31383  dmvlsiga  31388  sigainb  31395  measval  31457  ismeas  31458  sxbrsigalem0  31529  omssubadd  31558  carsggect  31576  eulerpartlemmf  31633  eulerpartlemgs2  31638  eulerpartlemn  31639  rrvsum  31712  ballotlem2  31746  ballotlemfcc  31751  ballotlem4  31756  signsplypnf  31820  signsply0  31821  signsw0glem  31823  signswrid  31828  signlem0  31857  signshf  31858  bnj535  32162  bnj580  32185  bnj907  32239  bnj1253  32289  funen1cnv  32357  loop1cycl  32384  ptpconn  32480  cvmsss2  32521  cvmlift2lem12  32561  cvmlift2lem13  32562  cvmliftphtlem  32564  cvmliftpht  32565  fmlafvel  32632  mppsthm  32826  bcneg1  32968  fv1stcnv  33020  fv2ndcnv  33021  trpred0  33075  wlimeq1  33107  frr3g  33121  fpr3g  33122  noextendseq  33174  noetalem3  33219  scutun12  33271  imagesset  33414  altopeq1  33424  brcolinear2  33519  cldbnd  33674  ivthALT  33683  refssfne  33706  ontgval  33779  onint1  33797  axc11n11r  34017  bj-bm1.3ii  34360  bj-restsn0  34379  bj-restsn10  34380  bj-restsnid  34381  bj-rest10  34382  bj-rest0  34387  bj-inftyexpiinv  34493  bj-inftyexpidisj  34495  taupilem1  34605  f1omptsnlem  34620  mptsnunlem  34622  topdifinffinlem  34631  inunissunidif  34659  rdgssun  34662  exrecfnlem  34663  exrecfnpw  34665  finixpnum  34892  tan2h  34899  matunitlindflem2  34904  ptrest  34906  poimirlem22  34929  poimirlem25  34932  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2addnclem  34958  itg2addnclem2  34959  itg2addnclem3  34960  itg2addnc  34961  itg2gt0cn  34962  ftc1anclem5  34986  ftc1anclem8  34989  dvasin  34993  dvacos  34994  sdclem2  35032  totbndbnd  35082  heibor1lem  35102  heiborlem7  35110  bfplem1  35115  prnc  35360  ecexALTV  35603  brxrn  35641  riotasv  36110  glbconN  36528  atpointN  36894  polsubN  37058  pol0N  37060  pol1N  37061  2polvalN  37065  2polssN  37066  3polN  37067  pcl0N  37073  2pmaplubN  37077  pnonsingN  37084  polsubclN  37103  cdlemefs32sn1aw  37565  cdleme43fsv1snlem  37571  cdleme41sn3a  37584  cdleme32a  37592  cdleme40m  37618  cdleme40n  37619  cdleme42b  37629  istendo  37911  cdlemk40  38068  cdlemkid  38087  dihvalcqpre  38386  fac2xp3  39143  facp2  39144  2xp3dxp2ge1d  39146  factwoffsmonot  39147  fnsnbt  39169  frlmsnic  39198  0prjspn  39319  3cubes  39336  mapfzcons1cl  39364  eldioph3b  39411  eldiophss  39420  0dioph  39424  vdioph  39425  eldioph4b  39457  eldioph4i  39458  rencldnfilem  39466  rmxy1  39568  rmxy0  39569  rmxm1  39580  rmym1  39581  monotoddzzfi  39588  aomclem6  39708  pwslnmlem0  39740  isnumbasabl  39755  areaquad  39872  relexp2  40071  eltrclrec  40074  elrtrclrec  40075  brtrclrec  40090  brrtrclrec  40091  relexpxpmin  40111  dftrcl3  40114  dfrtrcl3  40127  heeq1  40172  seff  40690  lhe4.4ex1a  40710  eelT0  41158  snssl  41213  sineq0ALT  41320  elabrexg  41352  elrnmpt1sf  41499  founiiun0  41500  supxrgere  41650  supxrgelem  41654  fmuldfeqlem1  41912  fmuldfeq  41913  climneg  41940  sumnnodd  41960  liminfltlem  42134  xlimpnfxnegmnf2  42188  addccncf2  42208  dvsinax  42246  stoweidlem18  42352  stoweidlem19  42353  stoweidlem22  42356  stoweidlem34  42368  stoweidlem40  42374  stoweidlem41  42375  stoweidlem55  42389  stoweidlem59  42393  dirker2re  42426  dirkerdenne0  42427  fourierdlem48  42488  fourierdlem49  42489  fourierdlem70  42510  fourierdlem71  42511  fourierdlem104  42544  fourierdlem112  42552  fouriersw  42565  etransclem46  42614  etransclem48  42616  nnfoctbdjlem  42786  sqrtnegnre  43556  fsummmodsnunz  43584  flsqrt5  43806  bits0ALTV  43893  mogoldbblem  43934  sgoldbeven3prm  43997  nnsum3primes4  44002  ushrisomgr  44055  2zrngnmlid  44269  2zrngnmrid  44270  mpoexxg2  44435  lco0  44531  zlmodzxzldeplem3  44606  0dig1  44718  aacllem  44951