Theorem mpan2 687

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 683	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 206  df-an 396

This theorem is referenced by:  mpanr12  701  mp3an23  1451  elvd  3429  eueq2  3640  sbcgf  3789  sbcralg  3803  csbconstgf  3846  sbcnestgw  4351  csbnestgw  4352  sbcnestg  4356  csbnestg  4357  csbnest1g  4360  mpteq1OLD  5164  iinexg  5260  eusv2nf  5313  reusv2lem5  5320  nnullss  5371  xpss1  5599  xpiindi  5733  reldm0  5826  elrnmpt1s  5855  resdm  5925  eliniseg  5991  trinxp  6019  ssrnres  6070  cnveq0  6089  coi2  6156  relrelss  6165  cnviin  6178  elpred  6208  ord0eln0  6305  funcnvres  6496  funimaex  6505  fnresin1  6541  fnresin2  6542  fresin  6627  ssimaex  6835  fvmpt  6857  fvmptnf  6879  fvimacnvALT  6916  dff3  6958  fsn  6989  fsn2  6990  funop  7003  fvrnressn  7015  fninfp  7028  fndifnfp  7030  fnnfpeq0  7032  fprb  7051  elabrex  7098  f1elima  7117  f1ofvswap  7158  fliftel1  7161  f1owe  7204  sorpssuni  7563  sorpssint  7564  eldifpw  7596  ordeleqon  7609  ordsson  7610  ssnlim  7707  tposfun  8029  tpostpos2  8034  fpr3g  8072  wfr3g  8109  wfrlem14OLD  8124  wfrlem15OLD  8125  tfrlem10  8189  tfrlem12  8191  tfr3  8201  seqomlem1  8251  seqomlem2  8252  seqomlem4  8254  ondif2  8294  oa0  8308  om0  8309  oa1suc  8323  om1  8335  oe1  8337  oe1m  8338  omass  8373  oeoalem  8389  oeoelem  8391  nnmsucr  8418  nnm1  8442  nnm2  8443  ecelqsg  8519  xpider  8535  mapdm0  8588  fvdiagfn  8637  ixpsnf1o  8684  xp1en  8798  sbthlem7  8829  domunsn  8863  xpmapenlem  8880  infensuc  8891  findcard2d  8911  cnvfi  8924  enreffi  8929  infi  8972  finresfin  8974  diffi  8979  unblem1  8996  unblem2  8997  unblem3  8998  unblem4  8999  isfinite2  9002  infn0  9006  unfilem1  9008  unfilem2  9009  unfir  9012  fofinf1o  9024  cnvfiALT  9031  pwfilemOLD  9043  mptfi  9048  finsschain  9056  marypha2  9128  inf0  9309  trpred0  9410  trcl  9417  frr3g  9445  r1rankidb  9493  snwf  9498  unwf  9499  uniwf  9508  rankval3b  9515  rankr1a  9525  rankxplim3  9570  scott0  9575  djueq1  9594  card1  9657  pm54.43  9690  infxpenc2  9709  dfac8clem  9719  alephsuc2  9767  alephle  9775  cardaleph  9776  dfac12lem2  9831  undjudom  9854  djudom1  9869  pwdju1  9877  nnadju  9884  ackbij1lem18  9924  cflem  9933  cflecard  9940  cfeq0  9943  cfslb  9953  cfsmolem  9957  cfcoflem  9959  cfidm  9962  isfin4p1  10002  fin23lem12  10018  fin23lem16  10022  fin23lem28  10027  fin23lem38  10036  fin23lem41  10039  fin1a2lem7  10093  fin1a2lem12  10098  fin1a2lem13  10099  hsmexlem8  10111  axcc2lem  10123  axcc3  10125  domtriomlem  10129  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  axcclem  10144  ac6num  10166  ttukeylem4  10199  ttukeylem7  10202  ttukey2g  10203  axdclem  10206  brdom3  10215  brdom5  10216  cardeq0  10239  unsnen  10240  konigthlem  10255  pwcfsdom  10270  canthp1lem1  10339  wunex2  10425  wuncval2  10434  eltsk2g  10438  ingru  10502  grutsk  10509  axgroth6  10515  mulidpi  10573  nlt1pi  10593  indpi  10594  pinq  10614  mulidnq  10650  1idpr  10716  prlem934  10720  0idsr  10784  1idsr  10785  00sr  10786  negexsr  10789  recexsrlem  10790  sqgt0sr  10793  ax1rid  10848  axcnre  10851  ne0gt0  11010  peano2cn  11077  peano2re  11078  00id  11080  mul02lem2  11082  mul01  11084  subid  11170  subid1  11171  negid  11198  negeq0  11205  peano2cnm  11217  peano2rem  11218  lt0neg1  11411  le0neg1  11413  relin01  11429  div2neg  11628  recgt0ii  11811  divgt0i2i  11820  ledivp1i  11830  ltdivp1i  11831  peano5nni  11906  peano2nn  11915  nnge1  11931  times2  12040  addltmul  12139  nn0p1nn  12202  peano2nn0  12203  nn0lele2xi  12218  frnnn0supp  12219  frnnn0fsupp  12220  frnnn0suppg  12221  peano2z  12291  peano2zm  12293  suprzcl  12330  zeo  12336  uzwo  12580  uzwo2  12581  infssuzle  12600  infssuzcl  12601  zq  12623  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  rphalfcl  12686  zgt1rpn0n1  12700  ltpnf  12785  nltmnf  12794  pnfge  12795  nltpnft  12827  xlemnf  12830  qsqueeze  12864  xlt0neg1  12882  xle0neg1  12884  xaddpnf1  12889  xaddmnf1  12891  xaddid1  12904  xsubge0  12924  xmul01  12930  xmulneg1  12932  xmulpnf1  12937  xmulid1  12942  supxrbnd  12991  supxrgtmnf  12992  supxrre1  12993  supxrre2  12994  elioopnf  13104  elicopnf  13106  iccshftri  13148  iccshftli  13150  iccdili  13152  icccntri  13154  fzprval  13246  fz0add1fz1  13385  fzofzp1  13412  fzostep1  13431  injresinj  13436  flge0nn0  13468  flge1nn  13469  btwnzge0  13476  modfrac  13532  om2uzsuci  13596  axdc4uzlem  13631  ser1const  13707  exp0  13714  exp1  13716  expn1  13720  nn0sqcl  13738  sqval  13763  sqeq0  13768  resqcl  13772  zsqcl  13776  expubnd  13823  binom21  13862  expnbnd  13875  nn0opthlem2  13911  bcnn  13954  bcn2  13961  bcn2p1  13967  bcnm1  13969  hasheq0  14006  hashsng  14012  hashen1  14013  hashunsnggt  14037  hashin  14054  hashdif  14056  hashgt23el  14067  hashxplem  14076  hashf1lem2  14098  hash2pr  14111  hash2prde  14112  pr2pwpr  14121  hash3tr  14132  iswrd  14147  wrdval  14148  hashwrdn  14178  ccatval2  14211  ccatrid  14220  eqs1  14245  s111  14248  ccatws1len  14253  repsw0  14418  repsw1  14424  cshw0  14435  wwlktovf  14599  relexpsucnnl  14669  reim0  14757  imval2  14790  cjne0  14802  abssq  14946  max0add  14950  abs2dif  14972  rddif  14980  absrdbnd  14981  rexuz3  14988  isershft  15303  isercolllem2  15305  isercoll  15307  fsum  15360  fsumadd  15380  fsumsplitsnun  15395  bcxmas  15475  infcvgaux2i  15498  fprod  15579  risefac0  15665  fallfac0  15666  risefac1  15671  fallfac1  15672  bpoly2  15695  bpoly3  15696  bpoly4  15697  fsumcube  15698  efi4p  15774  resin4p  15775  recos4p  15776  sinbnd  15817  cosbnd  15818  rpnnen2lem8  15858  rpnnen2lem12  15862  cnso  15884  dvdsmul2  15916  dvdslelem  15946  odd2np1lem  15977  mod2eq1n2dvds  15984  divalglem0  16030  divalglem1  16031  divalglem4  16033  divalglem5  16034  divalglem8  16037  flodddiv4  16050  bits0  16063  bitsp1o  16068  bitsf1  16081  sadadd2lem2  16085  gcd1  16163  gcdmultipleOLD  16188  lcm0val  16227  dvdslcm  16231  lcmeq0  16233  lcmgcd  16240  lcm1  16243  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  prm2orodd  16324  phiprm  16406  pc0  16483  pcdvdstr  16505  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  hashbc0  16634  setsval  16796  fsets  16798  setsres  16807  ressinbas  16881  ressress  16884  elrestr  17056  pwssnf1o  17126  xpsfrnel  17190  xpscf  17193  ismred2  17229  submre  17231  mreacs  17284  oppchomfval  17340  oppchomfvalOLD  17341  brssc  17443  isssc  17449  yonedalem4c  17911  oduleval  17923  isprs  17930  oduclatb  18140  gsumval2a  18284  smndex1n0mnd  18466  mulg1  18626  mulgnegnn  18629  isghm  18749  ghmghmrn  18768  cntrnsg  18863  oppgplusfval  18867  pgrpsubgsymg  18932  psgneldm2i  19028  efgrelexlemb  19271  frgp0  19281  frgpmhm  19286  vrgpf  19289  cntrcmnd  19358  cntrabl  19359  cygctb  19408  dprd0  19549  dprd2da  19560  mgpplusg  19639  opprmulfval  19779  subrgint  19961  lsp0  20186  sralemOLD  20355  rlmval2  20377  zringcyg  20603  mulgrhm2  20612  zlmsca  20638  chrnzr  20646  zrhpsgnelbas  20711  ocvz  20795  cssincl  20805  css0  20806  css1  20807  frlmip  20895  fczpsrbag  21036  ply1idvr1  21374  evls1rhmlem  21397  evl1fval1lem  21406  marrepeval  21620  decpmatid  21827  0opn  21961  topopn  21963  basdif0  22011  tgval  22013  isopn2  22091  0cld  22097  ntropn  22108  ntrval2  22110  ntrdif  22111  clsdif  22112  cmclsopn  22121  ntrtop  22129  ntr0  22140  mretopd  22151  neips  22172  neiptopnei  22191  maxlp  22206  isperf2  22211  rest0  22228  iocpnfordt  22274  icomnfordt  22275  mnfnei  22280  refref  22572  unisngl  22586  1stckgen  22613  ptbasfi  22640  pthaus  22697  fbssfi  22896  isfil2  22915  ssfg  22931  filconn  22942  fbasrn  22943  filufint  22979  imaelfm  23010  fmfnfmlem4  23016  fclsfnflim  23086  alexsubALTlem3  23108  alexsubALTlem4  23109  ustfilxp  23272  ustuqtop2  23302  ustuqtop4  23304  utopsnneiplem  23307  utopsnnei  23309  utop2nei  23310  cfiluweak  23355  neipcfilu  23356  xmetres  23425  metres  23426  mopnex  23581  prdsms  23593  metucn  23633  tngds  23717  tngdsOLD  23718  tngngp3  23726  nmoge0  23791  cnfldnm  23848  tgioo  23865  xrtgioo  23875  xrsmopn  23881  negcncf  23991  phtpy01  24054  pco0  24083  tcphtopn  24295  tchnmfval  24297  caussi  24366  rrxip  24459  minveclem3b  24497  ovolfioo  24536  ovolficc  24537  ovolfsf  24540  ovolctb  24559  ovolctb2  24561  ovolfiniun  24570  ovoliun2  24575  ovolshftlem1  24578  ovolscalem1  24582  ovolicopnf  24593  iunmbl2  24626  uniioombllem2  24652  opnmblALT  24672  ismbf  24697  mbfinf  24734  0plef  24741  itg1climres  24784  itg2cnlem1  24831  iblitg  24838  ibl0  24856  itgcn  24914  cnlimc  24957  dvfre  25020  dvnfre  25021  dveflem  25048  dvef  25049  dvlipcn  25063  lhop2  25084  itgsubstlem  25117  deg1val  25166  ply1rem  25233  coefv0  25314  plyrecj  25345  vieta1lem2  25376  aannenlem1  25393  aaliou2b  25406  ulmval  25444  ulmpm  25447  ulmdvlem1  25464  mtest  25468  efcn  25507  sin2pim  25547  cos2pim  25548  sinmpi  25549  cosmpi  25550  sinppi  25551  cosppi  25552  efimpi  25553  sincosq1lem  25559  sincosq2sgn  25561  sincosq3sgn  25562  sincosq4sgn  25563  sinq12gt0  25569  sinq34lt0t  25571  sincosq1eq  25574  abssinper  25582  efif1o  25607  loglt1b  25694  relogcn  25698  ellogdm  25699  efopn  25718  cxp0  25730  cxp1  25731  cxpsqrt  25763  logsqrt  25764  logb1  25824  atandm3  25933  atanbnd  25981  atancn  25991  leibpi  25997  efrlim  26024  logdifbnd  26048  vmaprm  26171  ppip1le  26215  ppieq0  26230  prmorcht  26232  ppiublem1  26255  ppiub  26257  chpeq0  26261  chtub  26265  fsumvma  26266  pclogsum  26268  chpval2  26271  dchrresb  26312  dchrptlem1  26317  lgs0  26363  lgs2  26367  lgsdir2lem2  26379  lgsdir2lem4  26381  lgsdchrval  26407  lgsdchr  26408  lgseisenlem2  26429  2lgslem1c  26446  2lgsoddprmlem2  26462  addsq2nreurex  26497  dirith2  26581  selberg2lem  26603  qabvle  26678  qabvexp  26679  ostth  26692  istrkg2ld  26725  istrkg3ld  26726  ttgval  27140  cchhllemOLD  27158  brbtwn  27170  colinearalglem4  27180  upgr0eop  27387  uspgrushgr  27448  usgruspgr  27451  usgr0eop  27516  0grsubgr  27548  uspgrloopvtx  27785  umgr2v2evtx  27791  usgr0edg0rusgr  27845  rgrusgrprc  27859  wlkvtxiedg  27894  pthdivtx  27998  usgr2pthlem  28032  wlkswwlksf1o  28145  wwlksext2clwwlk  28322  konigsbergssiedgw  28515  frgrncvvdeqlem7  28570  2clwwlk2  28613  ex-po  28700  pliguhgr  28749  nvnd  28951  ipval2lem3  28968  ipval2  28970  ipidsq  28973  dipcj  28977  dip0r  28980  nmlnogt0  29060  blocni  29068  ipasslem2  29095  ipasslem8  29100  ipasslem9  29101  ajval  29124  ubthlem1  29133  hvaddid2  29286  hvsub0  29339  hi02  29360  hlimi  29451  isch2  29486  chlimi  29497  chsupunss  29607  shsupunss  29609  chlejb1i  29739  h1dei  29813  h1de2ci  29819  spanunsni  29842  pjoml2i  29848  pjorthi  29932  mayete3i  29991  hosubid1  30061  nmopge0  30174  nmfnge0  30190  adj1  30196  adjeq  30198  lnop0  30229  lnopmi  30263  nmophmi  30294  cnlnadjlem5  30334  cnlnadjeui  30340  unierri  30367  leoprf2  30390  leopnmid  30401  nmopleid  30402  hstles  30494  hst0  30496  strlem3a  30515  dmdbr2  30566  mdsl1i  30584  mdsl2i  30585  mdsl2bi  30586  cvmdi  30587  mdslmd1lem1  30588  mdslmd1lem2  30589  mdslmd1i  30592  mdslmd2i  30593  csmdsymi  30597  mdexchi  30598  superpos  30617  atomli  30645  atordi  30647  chirredlem1  30653  chirredlem2  30654  atcvat4i  30660  atabsi  30664  mdsymlem1  30666  mdsymlem5  30670  mdsymlem6  30671  sumdmdii  30678  dmdbr5ati  30685  dmdbr6ati  30686  mddmdin0i  30694  cdj3lem2  30698  unidifsnel  30784  unidifsnne  30785  xppreima  30884  abfmpunirn  30891  abfmpel  30894  aciunf1lem  30901  fgreu  30911  imafi2  30948  padct  30956  fpwrelmapffslem  30969  fpwrelmap  30970  xrge0infss  30985  xrdifh  31003  pfx1s2  31115  clatp0cl  31156  clatp1cl  31157  cntrcrng  31224  cycpmco2lem4  31298  rmfsupp2  31394  resvval  31428  rearchi  31448  qusxpid  31461  locfinreflem  31692  locfinref  31693  ordtconnlem1  31776  rge0scvg  31801  lmxrge0  31804  qqh0  31834  qqh1  31835  rrh0  31865  zrhre  31869  esumcst  31931  esumfzf  31937  esumfsupre  31939  hasheuni  31953  sgon  31992  dmvlsiga  31997  sigainb  32004  measval  32066  ismeas  32067  sxbrsigalem0  32138  omssubadd  32167  carsggect  32185  eulerpartlemmf  32242  eulerpartlemgs2  32247  eulerpartlemn  32248  rrvsum  32321  ballotlem2  32355  ballotlemfcc  32360  ballotlem4  32365  signsplypnf  32429  signsply0  32430  signsw0glem  32432  signswrid  32437  signlem0  32466  signshf  32467  bnj535  32770  bnj580  32793  bnj907  32847  bnj1253  32897  funen1cnv  32960  loop1cycl  32999  ptpconn  33095  cvmsss2  33136  cvmlift2lem12  33176  cvmlift2lem13  33177  cvmliftphtlem  33179  cvmliftpht  33180  fmlafvel  33247  mppsthm  33441  onelssex  33563  bcneg1  33608  fv1stcnv  33657  fv2ndcnv  33658  wlimeq1  33741  naddid1  33763  noextendseq  33797  noetasuplem4  33866  noetainflem4  33870  scutun12  33931  madebdayim  33997  addsid1  34054  imagesset  34182  altopeq1  34192  brcolinear2  34287  cldbnd  34442  ivthALT  34451  refssfne  34474  ontgval  34547  onint1  34565  axc11n11r  34792  bj-pm11.53a  34887  bj-bm1.3ii  35162  bj-restsn0  35183  bj-restsn10  35184  bj-restsnid  35185  bj-rest10  35186  bj-rest0  35191  bj-inftyexpiinv  35306  bj-inftyexpidisj  35308  taupilem1  35419  irrdiff  35424  f1omptsnlem  35434  mptsnunlem  35436  topdifinffinlem  35445  inunissunidif  35473  rdgssun  35476  exrecfnlem  35477  exrecfnpw  35479  finixpnum  35689  tan2h  35696  matunitlindflem2  35701  ptrest  35703  poimirlem22  35726  poimirlem25  35729  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2addnclem  35755  itg2addnclem2  35756  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ftc1anclem5  35781  ftc1anclem8  35784  dvasin  35788  dvacos  35789  sdclem2  35827  totbndbnd  35874  heibor1lem  35894  heiborlem7  35902  bfplem1  35907  prnc  36152  ecexALTV  36393  brxrn  36431  riotasv  36900  glbconN  37318  atpointN  37684  polsubN  37848  pol0N  37850  pol1N  37851  2polvalN  37855  2polssN  37856  3polN  37857  pcl0N  37863  2pmaplubN  37867  pnonsingN  37874  polsubclN  37893  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme41sn3a  38374  cdleme32a  38382  cdleme40m  38408  cdleme40n  38409  cdleme42b  38419  istendo  38701  cdlemk40  38858  cdlemkid  38877  dihvalcqpre  39176  facp2  40027  fac2xp3  40088  2xp3dxp2ge1d  40090  factwoffsmonot  40091  fnsnbt  40134  frlmsnic  40188  relt0neg1  40346  sn-inelr  40356  prjspnerlem  40377  prjspnval2  40378  0prjspn  40386  3cubes  40428  mapfzcons1cl  40456  eldioph3b  40503  eldiophss  40512  0dioph  40516  vdioph  40517  eldioph4b  40549  eldioph4i  40550  rencldnfilem  40558  rmxy1  40660  rmxy0  40661  rmxm1  40672  rmym1  40673  monotoddzzfi  40680  wepwso  40784  aomclem6  40800  pwslnmlem0  40832  isnumbasabl  40847  areaquad  40963  reabsifneg  41129  reabsifnneg  41132  relexp2  41174  eltrclrec  41177  elrtrclrec  41178  brtrclrec  41193  brrtrclrec  41194  relexpxpmin  41214  dftrcl3  41217  dfrtrcl3  41230  heeq1  41274  seff  41816  lhe4.4ex1a  41836  eelT0  42284  snssl  42339  sineq0ALT  42446  elabrexg  42478  elrnmpt1sf  42616  founiiun0  42617  supxrgere  42762  supxrgelem  42766  fmuldfeqlem1  43013  fmuldfeq  43014  climneg  43041  sumnnodd  43061  liminfltlem  43235  xlimpnfxnegmnf2  43289  addccncf2  43307  dvsinax  43344  stoweidlem18  43449  stoweidlem19  43450  stoweidlem22  43453  stoweidlem34  43465  stoweidlem40  43471  stoweidlem41  43472  stoweidlem55  43486  stoweidlem59  43490  dirker2re  43523  dirkerdenne0  43524  fourierdlem48  43585  fourierdlem49  43586  fourierdlem70  43607  fourierdlem71  43608  fourierdlem104  43641  fourierdlem112  43649  fouriersw  43662  etransclem46  43711  etransclem48  43713  nnfoctbdjlem  43883  sqrtnegnre  44687  fsummmodsnunz  44715  flsqrt5  44934  bits0ALTV  45019  mogoldbblem  45060  sgoldbeven3prm  45123  nnsum3primes4  45128  ushrisomgr  45181  2zrngnmlid  45395  2zrngnmrid  45396  mpoexxg2  45561  lco0  45656  zlmodzxzldeplem3  45731  0dig1  45843  naryfvalel  45864  ackvalsuc0val  45921  aacllem  46391