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  3465  eueq2  3693  sbcgf  3836  sbcralg  3849  csbconstgf  3892  sbcnestgw  4398  csbnestgw  4399  sbcnestg  4403  csbnestg  4404  csbnest1g  4407  iinexg  5318  eusv2nf  5365  reusv2lem5  5372  nnullss  5437  xpss1  5673  xpiindi  5815  reldm0  5907  elrnmpt1s  5939  resdm  6013  eliniseg  6081  trinxp  6114  ssrnres  6167  cnveq0  6186  coi2  6252  relrelss  6262  cnviin  6275  elpred  6307  onelssex  6401  ord0eln0  6408  funcnvres  6613  funimaex  6624  fnresin1  6662  fnresin2  6663  fresin  6746  ssimaex  6963  fvmpt  6985  fvmptnf  7007  fvimacnvALT  7046  dff3  7089  fsn  7124  fsn2  7125  funop  7138  fvrnressn  7150  fnsnbg  7155  fninfp  7165  fndifnfp  7167  fnnfpeq0  7169  fprb  7185  elabrex  7233  elabrexg  7234  f1elima  7255  f1ofvswap  7298  fliftel1  7302  f1owe  7345  sorpssuni  7724  sorpssint  7725  eldifpw  7760  ordeleqon  7774  ordsson  7775  ssnlim  7879  abrexexg  7957  tposfun  8239  tpostpos2  8244  fpr3g  8282  wfr3g  8319  wfrlem14OLD  8334  wfrlem15OLD  8335  tfrlem10  8399  tfrlem12  8401  tfr3  8411  seqomlem1  8462  seqomlem2  8463  seqomlem4  8465  ondif2  8512  oa0  8526  om0  8527  oa1suc  8541  om1  8552  oe1  8554  oe1m  8555  omass  8590  oeoalem  8606  oeoelem  8608  nnmsucr  8635  nnm1  8662  nnm2  8663  naddrid  8693  naddlid  8694  ecelqsg  8784  xpider  8800  mapdm0  8854  fvdiagfn  8903  ixpsnf1o  8950  xp1en  9069  undom  9071  sbthlem7  9101  domunsn  9139  xpmapenlem  9156  infensuc  9167  findcard2d  9178  diffi  9187  cnvfi  9188  enreffi  9195  snnen2o  9243  1sdom2dom  9253  infi  9272  finresfin  9274  unblem1  9298  unblem2  9299  unblem3  9300  unblem4  9301  isfinite2  9304  infn0ALT  9311  unfilem1  9313  unfilem2  9314  unfir  9316  fofinf1o  9342  cnvfiALT  9349  mptfi  9361  finsschain  9369  marypha2  9449  inf0  9633  trcl  9740  frr3g  9768  r1rankidb  9816  snwf  9821  unwf  9822  uniwf  9831  rankval3b  9838  rankr1a  9848  rankxplim3  9893  scott0  9898  djueq1  9917  card1  9980  pm54.43  10013  infxpenc2  10034  dfac8clem  10044  alephsuc2  10092  alephle  10100  cardaleph  10101  dfac12lem2  10157  undjudom  10180  djudom1  10195  pwdju1  10203  nnadju  10210  ackbij1lem18  10248  cflem  10257  cflemOLD  10258  cflecard  10265  cfeq0  10268  cfslb  10278  cfsmolem  10282  cfcoflem  10284  cfidm  10287  isfin4p1  10327  fin23lem12  10343  fin23lem16  10347  fin23lem28  10352  fin23lem38  10361  fin23lem41  10364  fin1a2lem7  10418  fin1a2lem12  10423  fin1a2lem13  10424  hsmexlem8  10436  axcc2lem  10448  axcc3  10450  domtriomlem  10454  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  axcclem  10469  ac6num  10491  ttukeylem4  10524  ttukeylem7  10527  ttukey2g  10528  axdclem  10531  brdom3  10540  brdom5  10541  cardeq0  10564  unsnen  10565  konigthlem  10580  pwcfsdom  10595  canthp1lem1  10664  wunex2  10750  wuncval2  10759  eltsk2g  10763  ingru  10827  grutsk  10834  axgroth6  10840  mulidpi  10898  nlt1pi  10918  indpi  10919  pinq  10939  mulidnq  10975  1idpr  11041  prlem934  11045  0idsr  11109  1idsr  11110  00sr  11111  negexsr  11114  recexsrlem  11115  sqgt0sr  11118  ax1rid  11173  axcnre  11176  ne0gt0  11338  peano2cn  11405  peano2re  11406  00id  11408  mul02lem2  11410  mul01  11412  subid  11500  subid1  11501  negid  11528  negeq0  11535  peano2cnm  11547  peano2rem  11548  lt0neg1  11741  le0neg1  11743  relin01  11759  div2neg  11962  recgt0ii  12146  divgt0i2i  12155  ledivp1i  12165  ltdivp1i  12166  peano5nni  12241  peano2nn  12250  nnge1  12266  nnne0  12272  times2  12375  addltmul  12475  nn0p1nn  12538  peano2nn0  12539  nn0lele2xi  12555  fcdmnn0supp  12556  fcdmnn0fsupp  12557  fcdmnn0suppg  12558  peano2z  12631  peano2zm  12633  suprzcl  12671  zeo  12677  eluzaddi  12881  uzwo  12925  uzwo2  12926  infssuzle  12945  infssuzcl  12946  zq  12968  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem5  12995  rphalfcl  13034  zgt1rpn0n1  13048  ltpnf  13134  nltmnf  13143  pnfge  13144  nltpnft  13178  xlemnf  13181  qsqueeze  13215  xlt0neg1  13233  xle0neg1  13235  xaddpnf1  13240  xaddmnf1  13242  xaddrid  13255  xsubge0  13275  xmul01  13281  xmulneg1  13283  xmulpnf1  13288  xmulrid  13293  supxrbnd  13342  supxrgtmnf  13343  supxrre1  13344  supxrre2  13345  elioopnf  13458  elicopnf  13460  iccshftri  13502  iccshftli  13504  iccdili  13506  icccntri  13508  fzprval  13600  fz0add1fz1  13749  fzofzp1  13778  fzostep1  13797  injresinj  13802  flge0nn0  13835  flge1nn  13836  btwnzge0  13843  modfrac  13899  om2uzsuci  13964  axdc4uzlem  13999  ser1const  14074  exp0  14081  exp1  14083  expn1  14087  nn0sqcl  14105  sqval  14130  sqeq0  14136  resqcl  14140  zsqcl  14145  expubnd  14194  binom21  14235  expnbnd  14248  nn0opthlem2  14285  bcnn  14328  bcn2  14335  bcn2p1  14341  bcnm1  14343  hasheq0  14379  hashsng  14385  hashen1  14386  hashunsnggt  14410  hashin  14427  hashdif  14429  hashgt23el  14440  hashxplem  14449  hashf1lem2  14472  hash2pr  14485  hash2prde  14486  pr2pwpr  14495  hash3tr  14507  iswrd  14531  wrdval  14532  hashwrdn  14563  ccatval2  14594  ccatrid  14603  eqs1  14628  s111  14631  ccatws1len  14636  repsw0  14793  repsw1  14799  cshw0  14810  wwlktovf  14973  relexpsucnnl  15047  reim0  15135  imval2  15168  cjne0  15180  abssq  15323  max0add  15327  abs2dif  15349  rddif  15357  absrdbnd  15358  rexuz3  15365  isershft  15678  isercolllem2  15680  isercoll  15682  fsum  15734  fsumadd  15754  fsumsplitsnun  15769  bcxmas  15849  infcvgaux2i  15872  fprod  15955  risefac0  16041  fallfac0  16042  risefac1  16047  fallfac1  16048  bpoly2  16071  bpoly3  16072  bpoly4  16073  fsumcube  16074  efi4p  16153  resin4p  16154  recos4p  16155  sinbnd  16196  cosbnd  16197  rpnnen2lem8  16237  rpnnen2lem12  16241  cnso  16263  dvdsmul2  16296  dvdslelem  16326  odd2np1lem  16357  mod2eq1n2dvds  16364  divalglem0  16410  divalglem1  16411  divalglem4  16413  divalglem5  16414  divalglem8  16417  flodddiv4  16432  bits0  16445  bitsp1o  16450  bitsf1  16463  sadadd2lem2  16467  gcd1  16545  lcm0val  16611  dvdslcm  16615  lcmeq0  16617  lcmgcd  16624  lcm1  16627  lcmfunsnlem2lem2  16656  lcmfunsnlem2  16657  prm2orodd  16708  phiprm  16794  pc0  16872  pcdvdstr  16894  vdwlem2  17000  vdwlem6  17004  vdwlem8  17006  hashbc0  17023  setsval  17184  fsets  17186  setsres  17195  ressinbas  17264  ressress  17266  elrestr  17440  pwssnf1o  17510  xpsfrnel  17574  xpscf  17577  ismred2  17613  submre  17615  mreacs  17668  oppchomfval  17724  brssc  17825  isssc  17831  yonedalem4c  18287  oduleval  18299  isprs  18306  oduclatb  18515  gsumval2a  18661  smndex1n0mnd  18888  mulg1  19062  mulgnegnn  19065  isghmOLD  19197  ghmghmrn  19216  cntrnsg  19325  oppgplusfval  19329  pgrpsubgsymg  19388  psgneldm2i  19484  efgrelexlemb  19729  frgp0  19739  frgpmhm  19744  vrgpf  19747  cntrcmnd  19821  cntrabl  19822  cygctb  19871  dprd0  20012  dprd2da  20023  mgpplusg  20102  opprmulfval  20297  subrngint  20518  subrgint  20553  lsp0  20964  rlmval2  21148  cncrng  21349  cnfld1  21354  zringcyg  21428  mulgrhm2  21437  zlmsca  21479  fermltlchr  21488  chrnzr  21489  zrhpsgnelbas  21552  ocvz  21636  cssincl  21646  css0  21647  css1  21648  frlmip  21736  fczpsrbag  21879  ply1idvr1OLD  22231  evls1rhmlem  22257  evl1fval1lem  22266  marrepeval  22499  decpmatid  22706  0opn  22840  topopn  22842  basdif0  22889  tgval  22891  isopn2  22968  0cld  22974  ntropn  22985  ntrval2  22987  ntrdif  22988  clsdif  22989  cmclsopn  22998  ntrtop  23006  ntr0  23017  mretopd  23028  neips  23049  neiptopnei  23068  maxlp  23083  isperf2  23088  rest0  23105  iocpnfordt  23151  icomnfordt  23152  mnfnei  23157  refref  23449  unisngl  23463  1stckgen  23490  ptbasfi  23517  pthaus  23574  fbssfi  23773  isfil2  23792  ssfg  23808  filconn  23819  fbasrn  23820  filufint  23856  imaelfm  23887  fmfnfmlem4  23893  fclsfnflim  23963  alexsubALTlem3  23985  alexsubALTlem4  23986  ustfilxp  24149  ustuqtop2  24179  ustuqtop4  24181  utopsnneiplem  24184  utopsnnei  24186  utop2nei  24187  cfiluweak  24231  neipcfilu  24232  xmetres  24301  metres  24302  mopnex  24456  prdsms  24468  metucn  24508  tngds  24585  tngngp3  24593  nmoge0  24658  cnfldnm  24715  tgioo  24733  xrtgioo  24744  xrsmopn  24750  negcncf  24864  negcncfOLD  24865  phtpy01  24933  pco0  24963  tcphtopn  25176  tchnmfval  25178  caussi  25247  rrxip  25340  minveclem3b  25378  ovolfioo  25418  ovolficc  25419  ovolfsf  25422  ovolctb  25441  ovolctb2  25443  ovolfiniun  25452  ovoliun2  25457  ovolshftlem1  25460  ovolscalem1  25464  ovolicopnf  25475  iunmbl2  25508  uniioombllem2  25534  opnmblALT  25554  ismbf  25579  mbfinf  25616  0plef  25623  itg1climres  25665  itg2cnlem1  25712  iblitg  25719  ibl0  25738  itgcn  25796  cnlimc  25839  dvfre  25905  dvnfre  25906  dveflem  25933  dvef  25934  dvlipcn  25949  lhop2  25970  itgsubstlem  26005  deg1val  26051  ply1rem  26121  coefv0  26203  plyrecj  26237  vieta1lem2  26269  aannenlem1  26286  aaliou2b  26299  ulmval  26339  ulmpm  26342  ulmdvlem1  26359  mtest  26363  efcn  26403  sin2pim  26444  cos2pim  26445  sinmpi  26446  cosmpi  26447  sinppi  26448  cosppi  26449  efimpi  26450  sincosq1lem  26456  sincosq2sgn  26458  sincosq3sgn  26459  sincosq4sgn  26460  sinq12gt0  26466  sinq34lt0t  26468  sincosq1eq  26471  abssinper  26480  efif1o  26505  loglt1b  26593  relogcn  26597  ellogdm  26598  efopn  26617  cxp0  26629  cxp1  26630  cxpsqrt  26662  logsqrt  26663  logb1  26729  atandm3  26838  atanbnd  26886  atancn  26896  leibpi  26902  efrlim  26929  efrlimOLD  26930  logdifbnd  26954  vmaprm  27077  ppip1le  27121  ppieq0  27136  prmorcht  27138  ppiublem1  27163  ppiub  27165  chpeq0  27169  chtub  27173  fsumvma  27174  pclogsum  27176  chpval2  27179  dchrresb  27220  dchrptlem1  27225  lgs0  27271  lgs2  27275  lgsdir2lem2  27287  lgsdir2lem4  27289  lgsdchrval  27315  lgsdchr  27316  lgseisenlem2  27337  2lgslem1c  27354  2lgsoddprmlem2  27370  addsq2nreurex  27405  dirith2  27489  selberg2lem  27511  qabvle  27586  qabvexp  27587  ostth  27600  noextendseq  27629  noetasuplem4  27698  noetainflem4  27702  scutun12  27772  madebdayim  27843  addsrid  27914  addsfo  27933  peano2no  27934  negscl  27985  subsfo  28012  subsid1  28015  muls01  28055  mulsrid  28056  divs1  28146  recsex  28160  abssnid  28184  peano2ons  28205  noseqp1  28214  noseqind  28215  peano2nns  28270  dfnns2  28279  elzs2  28302  elnnzs  28304  elznns  28305  n0seo  28322  exps0  28327  exps1  28328  istrkg2ld  28385  istrkg3ld  28386  ttgval  28800  brbtwn  28824  colinearalglem4  28834  upgr0eop  29039  uspgrushgr  29102  usgruspgr  29105  usgr0eop  29171  0grsubgr  29203  uspgrloopvtx  29441  umgr2v2evtx  29447  usgr0edg0rusgr  29501  rgrusgrprc  29515  wlkvtxiedg  29551  pthdivtx  29655  usgr2pthlem  29691  wlkswwlksf1o  29807  wwlksext2clwwlk  29984  konigsbergssiedgw  30177  frgrncvvdeqlem7  30232  2clwwlk2  30275  ex-po  30362  pliguhgr  30413  nvnd  30615  ipval2lem3  30632  ipval2  30634  ipidsq  30637  dipcj  30641  dip0r  30644  nmlnogt0  30724  blocni  30732  ipasslem2  30759  ipasslem8  30764  ipasslem9  30765  ajval  30788  ubthlem1  30797  hvaddlid  30950  hvsub0  31003  hi02  31024  hlimi  31115  isch2  31150  chlimi  31161  chsupunss  31271  shsupunss  31273  chlejb1i  31403  h1dei  31477  h1de2ci  31483  spanunsni  31506  pjoml2i  31512  pjorthi  31596  mayete3i  31655  hosubid1  31725  nmopge0  31838  nmfnge0  31854  adj1  31860  adjeq  31862  lnop0  31893  lnopmi  31927  nmophmi  31958  cnlnadjlem5  31998  cnlnadjeui  32004  unierri  32031  leoprf2  32054  leopnmid  32065  nmopleid  32066  hstles  32158  hst0  32160  strlem3a  32179  dmdbr2  32230  mdsl1i  32248  mdsl2i  32249  mdsl2bi  32250  cvmdi  32251  mdslmd1lem1  32252  mdslmd1lem2  32253  mdslmd1i  32256  mdslmd2i  32257  csmdsymi  32261  mdexchi  32262  superpos  32281  atomli  32309  atordi  32311  chirredlem1  32317  chirredlem2  32318  atcvat4i  32324  atabsi  32328  mdsymlem1  32330  mdsymlem5  32334  mdsymlem6  32335  sumdmdii  32342  dmdbr5ati  32349  dmdbr6ati  32350  mddmdin0i  32358  cdj3lem2  32362  unidifsnel  32462  unidifsnne  32463  xppreima  32569  abfmpunirn  32576  abfmpel  32579  aciunf1lem  32586  fgreu  32596  imafi2  32635  padct  32643  fpwrelmapffslem  32655  fpwrelmap  32656  xrge0infss  32683  xrdifh  32703  pfx1s2  32860  clatp0cl  32902  clatp1cl  32903  cntrcrng  33010  cycpmco2lem4  33086  rmfsupp2  33179  1fldgenq  33262  resvval  33291  rearchi  33307  qusxpid  33324  opprabs  33443  zringfrac  33515  rlmdim  33595  constrfiss  33731  2sqr3minply  33760  locfinreflem  33817  locfinref  33818  ordtconnlem1  33901  rge0scvg  33926  lmxrge0  33929  qqh0  33961  qqh1  33962  rrh0  33992  zrhre  33996  esumcst  34040  esumfzf  34046  esumfsupre  34048  hasheuni  34062  sgon  34101  dmvlsiga  34106  sigainb  34113  measval  34175  ismeas  34176  sxbrsigalem0  34249  omssubadd  34278  carsggect  34296  eulerpartlemmf  34353  eulerpartlemgs2  34358  eulerpartlemn  34359  rrvsum  34432  ballotlem2  34467  ballotlemfcc  34472  ballotlem4  34477  signsplypnf  34528  signsply0  34529  signsw0glem  34531  signswrid  34536  signlem0  34565  signshf  34566  bnj535  34867  bnj580  34890  bnj907  34944  bnj1253  34994  funen1cnv  35065  loop1cycl  35105  ptpconn  35201  cvmsss2  35242  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmliftphtlem  35285  cvmliftpht  35286  fmlafvel  35353  mppsthm  35547  bcneg1  35699  fv1stcnv  35740  fv2ndcnv  35741  wlimeq1  35784  imagesset  35917  altopeq1  35927  brcolinear2  36022  cldbnd  36290  ivthALT  36299  refssfne  36322  ontgval  36395  onint1  36413  axc11n11r  36647  bj-pm11.53a  36742  bj-bm1.3ii  37028  bj-restsn0  37049  bj-restsn10  37050  bj-restsnid  37051  bj-rest10  37052  bj-rest0  37057  bj-inftyexpiinv  37172  bj-inftyexpidisj  37174  taupilem1  37285  irrdiff  37290  f1omptsnlem  37300  mptsnunlem  37302  topdifinffinlem  37311  inunissunidif  37339  rdgssun  37342  exrecfnlem  37343  exrecfnpw  37345  finixpnum  37575  tan2h  37582  matunitlindflem2  37587  ptrest  37589  poimirlem22  37612  poimirlem25  37615  mblfinlem1  37627  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  itg2addnclem  37641  itg2addnclem2  37642  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  ftc1anclem5  37667  ftc1anclem8  37670  dvasin  37674  dvacos  37675  sdclem2  37712  totbndbnd  37759  heibor1lem  37779  heiborlem7  37787  bfplem1  37792  prnc  38037  ecexALTV  38295  brxrn  38338  riotasv  38923  glbconN  39341  glbconNOLD  39342  atpointN  39708  polsubN  39872  pol0N  39874  pol1N  39875  2polvalN  39879  2polssN  39880  3polN  39881  pcl0N  39887  2pmaplubN  39891  pnonsingN  39898  polsubclN  39917  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdleme41sn3a  40398  cdleme32a  40406  cdleme40m  40432  cdleme40n  40433  cdleme42b  40443  istendo  40725  cdlemk40  40882  cdlemkid  40901  dihvalcqpre  41200  facp2  42102  fac2xp3  42198  2xp3dxp2ge1d  42200  factwoffsmonot  42201  relt0neg1  42434  sn-nnne0  42438  sn-inelr  42457  frlmsnic  42510  prjspnerlem  42587  prjspnval2  42588  0prjspn  42598  3cubes  42660  mapfzcons1cl  42688  eldioph3b  42735  eldiophss  42744  0dioph  42748  vdioph  42749  eldioph4b  42781  eldioph4i  42782  rencldnfilem  42790  rmxy1  42893  rmxy0  42894  rmxm1  42905  rmym1  42906  monotoddzzfi  42913  wepwso  43014  aomclem6  43030  pwslnmlem0  43062  isnumbasabl  43077  areaquad  43187  onexlimgt  43214  oaabsb  43265  nadd1suc  43363  om2  43375  oe2  43377  safesnsupfidom1o  43388  onno  43404  oa1cl  43418  finona1cl  43424  reabsifneg  43603  reabsifnneg  43606  relexp2  43648  eltrclrec  43651  elrtrclrec  43652  brtrclrec  43667  brrtrclrec  43668  relexpxpmin  43688  dftrcl3  43691  dfrtrcl3  43704  heeq1  43748  seff  44281  lhe4.4ex1a  44301  eelT0  44747  snssl  44802  sineq0ALT  44909  trfr  44935  xpwf  44937  dmwf  44938  rnwf  44939  modelaxreplem1  44951  modelaxreplem3  44953  0elaxnul  44956  prclaxpr  44958  uniclaxun  44959  wfac8prim  44975  permaxinf2lem  44985  elrnmpt1sf  45161  founiiun0  45162  supxrgere  45308  supxrgelem  45312  fmuldfeqlem1  45559  fmuldfeq  45560  climneg  45587  sumnnodd  45607  liminfltlem  45781  xlimpnfxnegmnf2  45835  addccncf2  45853  dvsinax  45890  stoweidlem18  45995  stoweidlem19  45996  stoweidlem22  45999  stoweidlem34  46011  stoweidlem40  46017  stoweidlem41  46018  stoweidlem55  46032  stoweidlem59  46036  dirker2re  46069  dirkerdenne0  46070  fourierdlem48  46131  fourierdlem49  46132  fourierdlem70  46153  fourierdlem71  46154  fourierdlem104  46187  fourierdlem112  46195  fouriersw  46208  etransclem46  46257  etransclem48  46259  nnfoctbdjlem  46432  ormklocald  46851  natlocalincr  46853  singoutnword  46859  sqrtnegnre  47284  fsummmodsnunz  47337  flsqrt5  47556  bits0ALTV  47641  mogoldbblem  47682  sgoldbeven3prm  47745  nnsum3primes4  47750  isubgr0uhgr  47834  ushggricedg  47888  2zrngnmlid  48178  2zrngnmrid  48179  mpoexxg2  48261  lco0  48351  zlmodzxzldeplem3  48426  0dig1  48537  naryfvalel  48558  ackvalsuc0val  48615  iinxp  48757  0funclem  48999  aacllem  49613