Theorem mpan2 678

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  mpanr12  692  mp3an23  1432  elvd  3422  eueq2  3616  sbcgf  3749  sbcralg  3761  csbconstgf  3799  sbcnestg  4261  csbnestg  4262  csbnest1g  4265  mpteq1  5015  iinexg  5100  eusv2nf  5149  reusv2lem5  5156  nnullss  5211  xpss1  5426  xpiindi  5556  reldm0  5641  elrnmpt1s  5672  resdm  5742  eliniseg  5798  trinxp  5825  ssrnres  5875  cnveq0  5893  coi2  5955  relrelss  5962  cnviin  5975  ord0eln0  6083  funcnvres  6265  funimaex  6274  fnresin1  6304  fnresin2  6305  fresin  6376  ssimaex  6576  fvmpt  6595  fvmptnf  6616  fvimacnvALT  6652  dff3  6689  fsn  6720  fsn2  6721  funop  6734  fvrnressn  6746  fninfp  6759  fndifnfp  6761  fnnfpeq0  6763  fprb  6783  elabrex  6827  f1elima  6846  fliftel1  6886  f1owe  6929  sorpssuni  7276  sorpssint  7277  eldifpw  7307  ordeleqon  7319  ordsson  7320  ssnlim  7414  tposfun  7711  tpostpos2  7716  wfr3g  7756  wfrlem14  7772  wfrlem15  7773  tfrlem10  7827  tfrlem12  7829  tfr3  7839  seqomlem1  7889  seqomlem2  7890  seqomlem4  7892  ondif2  7929  oa0  7943  om0  7944  oa1suc  7958  om1  7969  oe1  7971  oe1m  7972  omass  8007  oeoalem  8023  oeoelem  8025  nnmsucr  8052  nnm1  8075  nnm2  8076  ecelqsg  8152  xpider  8168  mapdm0  8221  fvdiagfn  8253  ixpsnf1o  8299  xp1en  8399  sbthlem7  8429  domunsn  8463  xpmapenlem  8480  infensuc  8491  infi  8537  finresfin  8539  diffi  8545  findcard2d  8555  unblem1  8565  unblem2  8566  unblem3  8567  unblem4  8568  isfinite2  8571  infn0  8575  unfilem1  8577  unfilem2  8578  unfir  8581  fofinf1o  8594  cnvfi  8601  pwfilem  8613  mptfi  8618  finsschain  8626  marypha2  8698  inf0  8878  trcl  8964  r1rankidb  9027  snwf  9032  unwf  9033  uniwf  9042  rankval3b  9049  rankr1a  9059  rankxplim3  9104  scott0  9109  djueq1  9128  card1  9191  pm54.43  9223  infxpenc2  9242  dfac8clem  9252  alephsuc2  9300  alephle  9308  cardaleph  9309  dfac12lem2  9364  cdaval  9389  cdadju  9390  undjudom  9391  djudom1  9406  pwdju1  9414  ackbij1lem18  9457  cflem  9466  cflecard  9473  cfeq0  9476  cfslb  9486  cfsmolem  9490  cfcoflem  9492  cfidm  9495  isfin4p1  9535  fin23lem12  9551  fin23lem16  9555  fin23lem28  9560  fin23lem38  9569  fin23lem41  9572  fin1a2lem7  9626  fin1a2lem12  9631  fin1a2lem13  9632  hsmexlem8  9644  axcc2lem  9656  axcc3  9658  domtriomlem  9662  axdc3lem2  9671  axdc3lem4  9673  axdc4lem  9675  axcclem  9677  ac6num  9699  ttukeylem4  9732  ttukeylem7  9735  ttukey2g  9736  axdclem  9739  brdom3  9748  brdom5  9749  cardeq0  9772  unsnen  9773  konigthlem  9788  pwcfsdom  9803  canthp1lem1  9872  wunex2  9958  wuncval2  9967  eltsk2g  9971  ingru  10035  grutsk  10042  axgroth6  10048  mulidpi  10106  nlt1pi  10126  indpi  10127  pinq  10147  mulidnq  10183  1idpr  10249  prlem934  10253  0idsr  10317  1idsr  10318  00sr  10319  negexsr  10322  recexsrlem  10323  sqgt0sr  10326  ax1rid  10381  axcnre  10384  ne0gt0  10545  peano2cn  10612  peano2re  10613  00id  10615  mul02lem2  10617  mul01  10619  subid  10706  subid1  10707  negid  10734  negeq0  10741  peano2cnm  10753  peano2rem  10754  lt0neg1  10947  le0neg1  10949  relin01  10965  div2neg  11164  recgt0ii  11347  divgt0i2i  11356  ledivp1i  11366  ltdivp1i  11367  peano5nni  11442  peano2nn  11453  nnge1  11468  times2  11584  addltmul  11683  nn0p1nn  11748  peano2nn0  11749  nn0lele2xi  11764  frnnn0fsupp  11766  peano2z  11836  peano2zm  11838  suprzcl  11875  zeo  11881  uzwo  12125  uzwo2  12126  infssuzle  12145  infssuzcl  12146  zq  12168  rpnnen1lem1  12192  rpnnen1lem3  12193  rpnnen1lem5  12195  rphalfcl  12233  zgt1rpn0n1  12247  ltpnf  12332  nltmnf  12341  pnfge  12342  nltpnft  12374  xlemnf  12377  qsqueeze  12411  xlt0neg1  12429  xle0neg1  12431  xaddpnf1  12436  xaddmnf1  12438  xaddid1  12451  xsubge0  12470  xmul01  12476  xmulneg1  12478  xmulpnf1  12483  xmulid1  12488  supxrbnd  12537  supxrgtmnf  12538  supxrre1  12539  supxrre2  12540  elioopnf  12647  elicopnf  12649  iccshftri  12689  iccshftli  12691  iccdili  12693  icccntri  12695  fzprval  12784  fz0add1fz1  12922  fzofzp1  12949  fzostep1  12968  injresinj  12973  flge0nn0  13005  flge1nn  13006  btwnzge0  13013  modfrac  13067  om2uzsuci  13131  axdc4uzlem  13166  ser1const  13241  exp0  13248  exp1  13250  expn1  13254  nn0sqcl  13271  sqval  13296  sqeq0  13301  resqcl  13305  zsqcl  13309  expubnd  13356  binom21  13395  expnbnd  13408  nn0opthlem2  13444  bcnn  13487  bcn2  13494  bcn2p1  13500  bcnm1  13502  hasheq0  13539  hashsng  13544  hashen1  13545  hashunsnggt  13568  hashin  13585  hashdif  13587  hashgt23el  13598  hashxplem  13607  hashf1lem2  13627  hash2pr  13638  hash2prde  13639  pr2pwpr  13648  hash3tr  13659  iswrd  13674  wrdval  13675  wrdvOLD  13689  hashwrdn  13709  ccatval2  13741  ccatrid  13750  s111  13778  swrd0len0OLD  13828  repsw0  13996  repsw1  14002  cshw0  14018  wwlktovf  14181  relexpsucnnl  14252  reim0  14338  imval2  14371  cjne0  14383  abssq  14527  max0add  14531  abs2dif  14553  rddif  14561  absrdbnd  14562  rexuz3  14569  isershft  14881  isercolllem2  14883  isercoll  14885  fsum  14937  fsumadd  14956  fsumsplitsnun  14970  bcxmas  15050  infcvgaux2i  15073  fprod  15155  risefac0  15241  fallfac0  15242  risefac1  15247  fallfac1  15248  bpoly2  15271  bpoly3  15272  bpoly4  15273  fsumcube  15274  efi4p  15350  resin4p  15351  recos4p  15352  sinbnd  15393  cosbnd  15394  rpnnen2lem8  15434  rpnnen2lem12  15438  cnso  15460  dvdsmul2  15492  dvdslelem  15519  odd2np1lem  15549  mod2eq1n2dvds  15556  divalglem0  15604  divalglem1  15605  divalglem4  15607  divalglem5  15608  divalglem8  15611  flodddiv4  15624  bits0  15637  bitsp1o  15642  bitsf1  15655  sadadd2lem2  15659  gcd1  15736  gcdmultiple  15756  lcm0val  15794  dvdslcm  15798  lcmeq0  15800  lcmgcd  15807  lcm1  15810  lcmfunsnlem2lem2  15839  lcmfunsnlem2  15840  prm2orodd  15891  phiprm  15970  pc0  16047  pcdvdstr  16068  vdwlem2  16174  vdwlem6  16178  vdwlem8  16180  hashbc0  16197  setsval  16369  fsets  16372  setsres  16381  ressinbas  16416  ressress  16418  elrestr  16558  pwssnf1o  16627  xpsfrnel  16692  ismred2  16732  submre  16734  mreacs  16787  oppchomfval  16842  brssc  16942  isssc  16948  yonedalem4c  17385  isprs  17398  oduleval  17599  oduclatb  17612  gsumval2a  17747  mulg1  18020  mulgnegnn  18023  isghm  18129  ghmghmrn  18148  cntrnsg  18243  oppgplusfval  18247  psgneldm2i  18395  efgrelexlemb  18636  frgp0  18646  frgpmhm  18651  vrgpf  18654  cygctb  18766  dprd0  18903  dprd2da  18914  mgpplusg  18966  opprmulfval  19098  subrgint  19280  lsp0  19503  sralem  19671  rlmval2  19688  fczpsrbag  19861  ply1idvr1  20164  evls1rhmlem  20187  evl1fval1lem  20195  zringcyg  20340  mulgrhm2  20348  zlmsca  20370  chrnzr  20379  zrhpsgnelbas  20440  ocvz  20524  cssincl  20534  css0  20535  css1  20536  frlmip  20624  marrepeval  20876  decpmatid  21082  0opn  21216  topopn  21218  basdif0  21265  tgval  21267  isopn2  21344  0cld  21350  ntropn  21361  ntrval2  21363  ntrdif  21364  clsdif  21365  cmclsopn  21374  ntrtop  21382  ntr0  21393  mretopd  21404  neips  21425  neiptopnei  21444  maxlp  21459  isperf2  21464  rest0  21481  iocpnfordt  21527  icomnfordt  21528  mnfnei  21533  refref  21825  unisngl  21839  1stckgen  21866  ptbasfi  21893  pthaus  21950  fbssfi  22149  isfil2  22168  ssfg  22184  filconn  22195  fbasrn  22196  filufint  22232  imaelfm  22263  fmfnfmlem4  22269  fclsfnflim  22339  alexsubALTlem3  22361  alexsubALTlem4  22362  ustfilxp  22524  ustuqtop2  22554  ustuqtop4  22556  utopsnneiplem  22559  utopsnnei  22561  utop2nei  22562  cfiluweak  22607  neipcfilu  22608  xmetres  22677  metres  22678  mopnex  22832  prdsms  22844  metucn  22884  tngds  22960  tngngp3  22968  nmoge0  23033  cnfldnm  23090  tgioo  23107  xrtgioo  23117  xrsmopn  23123  negcncf  23229  phtpy01  23292  pco0  23321  tcphtopn  23532  tchnmfval  23534  caussi  23603  rrxip  23696  minveclem3b  23734  ovolfioo  23771  ovolficc  23772  ovolfsf  23775  ovolctb  23794  ovolctb2  23796  ovolfiniun  23805  ovoliun2  23810  ovolshftlem1  23813  ovolscalem1  23817  ovolicopnf  23828  iunmbl2  23861  uniioombllem2  23887  opnmblALT  23907  ismbf  23932  mbfinf  23969  0plef  23976  itg1climres  24018  itg2cnlem1  24065  iblitg  24072  ibl0  24090  itgcn  24146  cnlimc  24189  dvfre  24251  dvnfre  24252  dveflem  24279  dvef  24280  dvlipcn  24294  lhop2  24315  itgsubstlem  24348  deg1val  24393  ply1rem  24460  coefv0  24541  plyrecj  24572  vieta1lem2  24603  aannenlem1  24620  aaliou2b  24633  ulmval  24671  ulmpm  24674  ulmdvlem1  24691  mtest  24695  efcn  24734  sin2pim  24774  cos2pim  24775  sinmpi  24776  cosmpi  24777  sinppi  24778  cosppi  24779  efimpi  24780  sincosq1lem  24786  sincosq2sgn  24788  sincosq3sgn  24789  sincosq4sgn  24790  sinq12gt0  24796  sinq34lt0t  24798  sincosq1eq  24801  abssinper  24809  efif1o  24831  loglt1b  24918  relogcn  24922  ellogdm  24923  efopn  24942  cxp0  24954  cxp1  24955  cxpsqrt  24987  logsqrt  24988  logb1  25048  atandm3  25157  atanbnd  25205  atancn  25215  leibpi  25222  efrlim  25249  logdifbnd  25273  vmaprm  25396  ppip1le  25440  ppieq0  25455  prmorcht  25457  ppiublem1  25480  ppiub  25482  chpeq0  25486  chtub  25490  fsumvma  25491  pclogsum  25493  chpval2  25496  dchrresb  25537  dchrptlem1  25542  lgs0  25588  lgs2  25592  lgsdir2lem2  25604  lgsdir2lem4  25606  lgsdchrval  25632  lgsdchr  25633  lgseisenlem2  25654  2lgslem1c  25671  2lgsoddprmlem2  25687  addsq2nreurex  25722  dirith2  25806  selberg2lem  25828  qabvle  25903  qabvexp  25904  ostth  25917  istrkg2ld  25948  istrkg3ld  25949  ttgval  26364  cchhllem  26376  brbtwn  26388  colinearalglem4  26398  upgr0eop  26602  uspgrushgr  26663  usgruspgr  26666  usgr0eop  26731  0grsubgr  26763  uspgrloopvtx  27000  umgr2v2evtx  27006  usgr0edg0rusgr  27060  rgrusgrprc  27074  wlkvtxiedg  27109  pthdivtx  27218  usgr2pthlem  27252  wlkswwlksf1o  27365  wwlksext2clwwlk  27580  konigsbergssiedgw  27782  frgrncvvdeqlem7  27839  2clwwlk2  27885  ex-po  27992  pliguhgr  28040  nvnd  28242  ipval2lem3  28259  ipval2  28261  ipidsq  28264  dipcj  28268  dip0r  28271  nmlnogt0  28351  blocni  28359  ipasslem2  28386  ipasslem8  28391  ipasslem9  28392  ajval  28416  ubthlem1  28425  hvaddid2  28579  hvsub0  28632  hi02  28653  hlimi  28744  isch2  28779  chlimi  28790  chsupunss  28902  shsupunss  28904  chlejb1i  29034  h1dei  29108  h1de2ci  29114  spanunsni  29137  pjoml2i  29143  pjorthi  29227  mayete3i  29286  hosubid1  29356  nmopge0  29469  nmfnge0  29485  adj1  29491  adjeq  29493  lnop0  29524  lnopmi  29558  nmophmi  29589  cnlnadjlem5  29629  cnlnadjeui  29635  unierri  29662  leoprf2  29685  leopnmid  29696  nmopleid  29697  hstles  29789  hst0  29791  strlem3a  29810  dmdbr2  29861  mdsl1i  29879  mdsl2i  29880  mdsl2bi  29881  cvmdi  29882  mdslmd1lem1  29883  mdslmd1lem2  29884  mdslmd1i  29887  mdslmd2i  29888  csmdsymi  29892  mdexchi  29893  superpos  29912  atomli  29940  atordi  29942  chirredlem1  29948  chirredlem2  29949  atcvat4i  29955  atabsi  29959  mdsymlem1  29961  mdsymlem5  29965  mdsymlem6  29966  sumdmdii  29973  dmdbr5ati  29980  dmdbr6ati  29981  mddmdin0i  29989  cdj3lem2  29993  xppreima  30156  abfmpunirn  30159  abfmpel  30162  aciunf1lem  30169  fgreu  30179  imafi2  30199  padct  30207  fpwrelmapffslem  30220  fpwrelmap  30221  xrge0infss  30236  xrdifh  30255  clatp0cl  30387  clatp1cl  30388  cntrcmnd  30530  cntrabl  30531  cntrcrng  30532  rmfsupp2  30542  resvval  30576  rearchi  30591  locfinreflem  30745  locfinref  30746  ordtconnlem1  30808  rge0scvg  30833  lmxrge0  30836  qqh0  30866  qqh1  30867  rrh0  30897  zrhre  30901  esumcst  30963  esumfzf  30969  esumfsupre  30971  hasheuni  30985  sgon  31025  dmvlsiga  31030  sigainb  31037  measval  31099  ismeas  31100  sxbrsigalem0  31171  omssubadd  31200  carsggect  31218  eulerpartlemmf  31275  eulerpartlemgs2  31280  eulerpartlemn  31281  rrvsum  31355  ballotlem2  31389  ballotlemfcc  31394  ballotlem4  31399  signsplypnf  31463  signsply0  31464  signsw0glem  31466  signswrid  31471  signlem0  31502  bnj535  31806  bnj580  31829  bnj907  31881  bnj1253  31931  ptpconn  32062  cvmsss2  32103  cvmlift2lem12  32143  cvmlift2lem13  32144  cvmliftphtlem  32146  cvmliftpht  32147  fmlafvel  32192  mppsthm  32343  bcneg1  32485  fv1stcnv  32537  fv2ndcnv  32538  trpred0  32593  wlimeq1  32625  frr3g  32639  fpr3g  32640  noextendseq  32692  noetalem3  32737  scutun12  32789  imagesset  32932  altopeq1  32942  brcolinear2  33037  cldbnd  33192  ivthALT  33201  refssfne  33224  ontgval  33296  onint1  33314  axc11n11r  33524  bj-bm1.3ii  33863  bj-restsn10  33884  bj-restsnid  33885  bj-rest10  33886  bj-rest0  33891  bj-inftyexpiinv  33956  bj-inftyexpidisj  33958  taupilem1  34041  f1omptsnlem  34056  mptsnunlem  34058  topdifinffinlem  34067  inunissunidif  34095  rdgssun  34098  exrecfnlem  34099  exrecfnpw  34101  finixpnum  34315  tan2h  34322  matunitlindflem2  34327  ptrest  34329  poimirlem22  34352  poimirlem25  34355  mblfinlem1  34367  mblfinlem2  34368  mblfinlem3  34369  mblfinlem4  34370  ismblfin  34371  itg2addnclem  34381  itg2addnclem2  34382  itg2addnclem3  34383  itg2addnc  34384  itg2gt0cn  34385  ftc1anclem5  34409  ftc1anclem8  34412  dvasin  34416  dvacos  34417  sdclem2  34456  totbndbnd  34506  heibor1lem  34526  heiborlem7  34534  bfplem1  34539  prnc  34784  ecexALTV  35030  brxrn  35068  riotasv  35537  glbconN  35955  atpointN  36321  polsubN  36485  pol0N  36487  pol1N  36488  2polvalN  36492  2polssN  36493  3polN  36494  pcl0N  36500  2pmaplubN  36504  pnonsingN  36511  polsubclN  36530  cdlemefs32sn1aw  36992  cdleme43fsv1snlem  36998  cdleme41sn3a  37011  cdleme32a  37019  cdleme40m  37045  cdleme40n  37046  cdleme42b  37056  istendo  37338  cdlemk40  37495  cdlemkid  37514  dihvalcqpre  37813  fnsnbt  38562  frlmsnic  38583  0prjspn  38674  mapfzcons1cl  38707  eldioph3b  38754  eldiophss  38764  0dioph  38768  vdioph  38769  eldioph4b  38801  eldioph4i  38802  rencldnfilem  38810  rmxy1  38912  rmxy0  38913  rmxm1  38924  rmym1  38925  monotoddzzfi  38932  aomclem6  39052  pwslnmlem0  39084  isnumbasabl  39099  areaquad  39216  relexp2  39382  eltrclrec  39385  elrtrclrec  39386  brtrclrec  39401  brrtrclrec  39402  relexpxpmin  39422  dftrcl3  39425  dfrtrcl3  39438  heeq1  39483  seff  40054  lhe4.4ex1a  40074  eelT0  40525  snssl  40580  sineq0ALT  40687  elabrexg  40719  elrnmpt1sf  40872  founiiun0  40873  mapdm0OLD  40879  supxrgere  41028  supxrgelem  41032  fmuldfeqlem1  41292  fmuldfeq  41293  climneg  41320  sumnnodd  41340  liminfltlem  41514  xlimpnfxnegmnf2  41568  addccncf2  41587  dvsinax  41625  stoweidlem18  41732  stoweidlem19  41733  stoweidlem22  41736  stoweidlem34  41748  stoweidlem40  41754  stoweidlem41  41755  stoweidlem55  41769  stoweidlem59  41773  dirker2re  41806  dirkerdenne0  41807  fourierdlem48  41868  fourierdlem49  41869  fourierdlem70  41890  fourierdlem71  41891  fourierdlem104  41924  fourierdlem112  41932  fouriersw  41945  etransclem46  41994  etransclem48  41996  nnfoctbdjlem  42166  sqrtnegnre  42911  fsummmodsnunz  42939  flsqrt5  43123  bits0ALTV  43210  mogoldbblem  43251  sgoldbeven3prm  43314  nnsum3primes4  43319  ushrisomgr  43372  2zrngnmlid  43582  2zrngnmrid  43583  mpt2exxg2  43748  lco0  43847  zlmodzxzldeplem3  43922  0dig1  44035  aacllem  44267