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 394

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 395

This theorem is referenced by:  mpanr12  703  mp3an23  1449  elvd  3468  eueq2  3702  sbcgf  3850  sbcralg  3864  csbconstgf  3907  sbcnestgw  4422  csbnestgw  4423  sbcnestg  4427  csbnestg  4428  csbnest1g  4431  mpteq1OLD  5243  iinexg  5344  eusv2nf  5395  reusv2lem5  5402  nnullss  5464  xpss1  5697  xpiindi  5838  reldm0  5930  elrnmpt1s  5959  resdm  6031  eliniseg  6099  trinxp  6132  ssrnres  6184  cnveq0  6203  coi2  6269  relrelss  6279  cnviin  6292  elpred  6324  onelssex  6419  ord0eln0  6426  funcnvres  6632  funimaex  6642  fnresin1  6681  fnresin2  6682  fresin  6766  ssimaex  6982  fvmpt  7004  fvmptnf  7026  fvimacnvALT  7065  dff3  7109  fsn  7144  fsn2  7145  funop  7158  fvrnressn  7170  fninfp  7183  fndifnfp  7185  fnnfpeq0  7187  fprb  7206  elabrex  7252  elabrexg  7253  f1elima  7273  f1ofvswap  7314  fliftel1  7317  f1owe  7360  sorpssuni  7738  sorpssint  7739  eldifpw  7771  ordeleqon  7785  ordsson  7786  ssnlim  7891  abrexexg  7965  tposfun  8248  tpostpos2  8253  fpr3g  8291  wfr3g  8328  wfrlem14OLD  8343  wfrlem15OLD  8344  tfrlem10  8408  tfrlem12  8410  tfr3  8420  seqomlem1  8471  seqomlem2  8472  seqomlem4  8474  ondif2  8523  oa0  8537  om0  8538  oa1suc  8552  om1  8563  oe1  8565  oe1m  8566  omass  8601  oeoalem  8617  oeoelem  8619  nnmsucr  8646  nnm1  8673  nnm2  8674  naddrid  8704  naddlid  8705  ecelqsg  8791  xpider  8807  mapdm0  8861  fvdiagfn  8910  ixpsnf1o  8957  xp1en  9082  undom  9084  sbthlem7  9114  domunsn  9152  xpmapenlem  9169  infensuc  9180  findcard2d  9191  diffi  9204  cnvfi  9205  enreffi  9211  snnen2o  9262  1sdom2dom  9272  infi  9293  finresfin  9295  unblem1  9320  unblem2  9321  unblem3  9322  unblem4  9323  isfinite2  9326  infn0ALT  9333  unfilem1  9335  unfilem2  9336  unfir  9339  fofinf1o  9353  cnvfiALT  9360  pwfilemOLD  9372  mptfi  9377  finsschain  9385  marypha2  9464  inf0  9646  trcl  9753  frr3g  9781  r1rankidb  9829  snwf  9834  unwf  9835  uniwf  9844  rankval3b  9851  rankr1a  9861  rankxplim3  9906  scott0  9911  djueq1  9930  card1  9993  pm54.43  10026  infxpenc2  10047  dfac8clem  10057  alephsuc2  10105  alephle  10113  cardaleph  10114  dfac12lem2  10169  undjudom  10192  djudom1  10207  pwdju1  10215  nnadju  10222  ackbij1lem18  10262  cflem  10271  cflecard  10278  cfeq0  10281  cfslb  10291  cfsmolem  10295  cfcoflem  10297  cfidm  10300  isfin4p1  10340  fin23lem12  10356  fin23lem16  10360  fin23lem28  10365  fin23lem38  10374  fin23lem41  10377  fin1a2lem7  10431  fin1a2lem12  10436  fin1a2lem13  10437  hsmexlem8  10449  axcc2lem  10461  axcc3  10463  domtriomlem  10467  axdc3lem2  10476  axdc3lem4  10478  axdc4lem  10480  axcclem  10482  ac6num  10504  ttukeylem4  10537  ttukeylem7  10540  ttukey2g  10541  axdclem  10544  brdom3  10553  brdom5  10554  cardeq0  10577  unsnen  10578  konigthlem  10593  pwcfsdom  10608  canthp1lem1  10677  wunex2  10763  wuncval2  10772  eltsk2g  10776  ingru  10840  grutsk  10847  axgroth6  10853  mulidpi  10911  nlt1pi  10931  indpi  10932  pinq  10952  mulidnq  10988  1idpr  11054  prlem934  11058  0idsr  11122  1idsr  11123  00sr  11124  negexsr  11127  recexsrlem  11128  sqgt0sr  11131  ax1rid  11186  axcnre  11189  ne0gt0  11351  peano2cn  11418  peano2re  11419  00id  11421  mul02lem2  11423  mul01  11425  subid  11511  subid1  11512  negid  11539  negeq0  11546  peano2cnm  11558  peano2rem  11559  lt0neg1  11752  le0neg1  11754  relin01  11770  div2neg  11970  recgt0ii  12153  divgt0i2i  12162  ledivp1i  12172  ltdivp1i  12173  peano5nni  12248  peano2nn  12257  nnge1  12273  nnne0  12279  times2  12382  addltmul  12481  nn0p1nn  12544  peano2nn0  12545  nn0lele2xi  12560  fcdmnn0supp  12561  fcdmnn0fsupp  12562  fcdmnn0suppg  12563  peano2z  12636  peano2zm  12638  suprzcl  12675  zeo  12681  eluzaddi  12886  uzwo  12928  uzwo2  12929  infssuzle  12948  infssuzcl  12949  zq  12971  rpnnen1lem1  12995  rpnnen1lem3  12996  rpnnen1lem5  12998  rphalfcl  13036  zgt1rpn0n1  13050  ltpnf  13135  nltmnf  13144  pnfge  13145  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  13455  elicopnf  13457  iccshftri  13499  iccshftli  13501  iccdili  13503  icccntri  13505  fzprval  13597  fz0add1fz1  13737  fzofzp1  13765  fzostep1  13784  injresinj  13789  flge0nn0  13821  flge1nn  13822  btwnzge0  13829  modfrac  13885  om2uzsuci  13949  axdc4uzlem  13984  ser1const  14059  exp0  14066  exp1  14068  expn1  14072  nn0sqcl  14090  sqval  14115  sqeq0  14120  resqcl  14124  zsqcl  14129  expubnd  14177  binom21  14217  expnbnd  14230  nn0opthlem2  14264  bcnn  14307  bcn2  14314  bcn2p1  14320  bcnm1  14322  hasheq0  14358  hashsng  14364  hashen1  14365  hashunsnggt  14389  hashin  14406  hashdif  14408  hashgt23el  14419  hashxplem  14428  hashf1lem2  14453  hash2pr  14466  hash2prde  14467  pr2pwpr  14476  hash3tr  14487  iswrd  14502  wrdval  14503  hashwrdn  14533  ccatval2  14564  ccatrid  14573  eqs1  14598  s111  14601  ccatws1len  14606  repsw0  14763  repsw1  14769  cshw0  14780  wwlktovf  14943  relexpsucnnl  15013  reim0  15101  imval2  15134  cjne0  15146  abssq  15289  max0add  15293  abs2dif  15315  rddif  15323  absrdbnd  15324  rexuz3  15331  isershft  15646  isercolllem2  15648  isercoll  15650  fsum  15702  fsumadd  15722  fsumsplitsnun  15737  bcxmas  15817  infcvgaux2i  15840  fprod  15921  risefac0  16007  fallfac0  16008  risefac1  16013  fallfac1  16014  bpoly2  16037  bpoly3  16038  bpoly4  16039  fsumcube  16040  efi4p  16117  resin4p  16118  recos4p  16119  sinbnd  16160  cosbnd  16161  rpnnen2lem8  16201  rpnnen2lem12  16205  cnso  16227  dvdsmul2  16259  dvdslelem  16289  odd2np1lem  16320  mod2eq1n2dvds  16327  divalglem0  16373  divalglem1  16374  divalglem4  16376  divalglem5  16377  divalglem8  16380  flodddiv4  16393  bits0  16406  bitsp1o  16411  bitsf1  16424  sadadd2lem2  16428  gcd1  16506  lcm0val  16568  dvdslcm  16572  lcmeq0  16574  lcmgcd  16581  lcm1  16584  lcmfunsnlem2lem2  16613  lcmfunsnlem2  16614  prm2orodd  16665  phiprm  16749  pc0  16826  pcdvdstr  16848  vdwlem2  16954  vdwlem6  16958  vdwlem8  16960  hashbc0  16977  setsval  17139  fsets  17141  setsres  17150  ressinbas  17229  ressress  17232  elrestr  17413  pwssnf1o  17483  xpsfrnel  17547  xpscf  17550  ismred2  17586  submre  17588  mreacs  17641  oppchomfval  17697  oppchomfvalOLD  17698  brssc  17800  isssc  17806  yonedalem4c  18272  oduleval  18284  isprs  18292  oduclatb  18502  gsumval2a  18648  smndex1n0mnd  18872  mulg1  19044  mulgnegnn  19047  isghmOLD  19179  ghmghmrn  19198  cntrnsg  19307  oppgplusfval  19311  pgrpsubgsymg  19376  psgneldm2i  19472  efgrelexlemb  19717  frgp0  19727  frgpmhm  19732  vrgpf  19735  cntrcmnd  19809  cntrabl  19810  cygctb  19859  dprd0  20000  dprd2da  20011  mgpplusg  20090  opprmulfval  20287  subrngint  20509  subrgint  20546  lsp0  20905  sralemOLD  21074  rlmval2  21097  cncrng  21333  cnfld1  21338  zringcyg  21412  mulgrhm2  21421  zlmsca  21467  fermltlchr  21476  chrnzr  21477  zrhpsgnelbas  21543  ocvz  21627  cssincl  21637  css0  21638  css1  21639  frlmip  21729  fczpsrbag  21873  ply1idvr1  22239  evls1rhmlem  22265  evl1fval1lem  22274  marrepeval  22509  decpmatid  22716  0opn  22850  topopn  22852  basdif0  22900  tgval  22902  isopn2  22980  0cld  22986  ntropn  22997  ntrval2  22999  ntrdif  23000  clsdif  23001  cmclsopn  23010  ntrtop  23018  ntr0  23029  mretopd  23040  neips  23061  neiptopnei  23080  maxlp  23095  isperf2  23100  rest0  23117  iocpnfordt  23163  icomnfordt  23164  mnfnei  23169  refref  23461  unisngl  23475  1stckgen  23502  ptbasfi  23529  pthaus  23586  fbssfi  23785  isfil2  23804  ssfg  23820  filconn  23831  fbasrn  23832  filufint  23868  imaelfm  23899  fmfnfmlem4  23905  fclsfnflim  23975  alexsubALTlem3  23997  alexsubALTlem4  23998  ustfilxp  24161  ustuqtop2  24191  ustuqtop4  24193  utopsnneiplem  24196  utopsnnei  24198  utop2nei  24199  cfiluweak  24244  neipcfilu  24245  xmetres  24314  metres  24315  mopnex  24472  prdsms  24484  metucn  24524  tngds  24608  tngdsOLD  24609  tngngp3  24617  nmoge0  24682  cnfldnm  24739  tgioo  24756  xrtgioo  24766  xrsmopn  24772  negcncf  24886  negcncfOLD  24887  phtpy01  24955  pco0  24985  tcphtopn  25198  tchnmfval  25200  caussi  25269  rrxip  25362  minveclem3b  25400  ovolfioo  25440  ovolficc  25441  ovolfsf  25444  ovolctb  25463  ovolctb2  25465  ovolfiniun  25474  ovoliun2  25479  ovolshftlem1  25482  ovolscalem1  25486  ovolicopnf  25497  iunmbl2  25530  uniioombllem2  25556  opnmblALT  25576  ismbf  25601  mbfinf  25638  0plef  25645  itg1climres  25688  itg2cnlem1  25735  iblitg  25742  ibl0  25760  itgcn  25818  cnlimc  25861  dvfre  25927  dvnfre  25928  dveflem  25955  dvef  25956  dvlipcn  25971  lhop2  25992  itgsubstlem  26027  deg1val  26076  ply1rem  26145  coefv0  26227  plyrecj  26259  vieta1lem2  26291  aannenlem1  26308  aaliou2b  26321  ulmval  26361  ulmpm  26364  ulmdvlem1  26381  mtest  26385  efcn  26425  sin2pim  26465  cos2pim  26466  sinmpi  26467  cosmpi  26468  sinppi  26469  cosppi  26470  efimpi  26471  sincosq1lem  26477  sincosq2sgn  26479  sincosq3sgn  26480  sincosq4sgn  26481  sinq12gt0  26487  sinq34lt0t  26489  sincosq1eq  26492  abssinper  26500  efif1o  26525  loglt1b  26613  relogcn  26617  ellogdm  26618  efopn  26637  cxp0  26649  cxp1  26650  cxpsqrt  26682  logsqrt  26683  logb1  26746  atandm3  26855  atanbnd  26903  atancn  26913  leibpi  26919  efrlim  26946  efrlimOLD  26947  logdifbnd  26971  vmaprm  27094  ppip1le  27138  ppieq0  27153  prmorcht  27155  ppiublem1  27180  ppiub  27182  chpeq0  27186  chtub  27190  fsumvma  27191  pclogsum  27193  chpval2  27196  dchrresb  27237  dchrptlem1  27242  lgs0  27288  lgs2  27292  lgsdir2lem2  27304  lgsdir2lem4  27306  lgsdchrval  27332  lgsdchr  27333  lgseisenlem2  27354  2lgslem1c  27371  2lgsoddprmlem2  27387  addsq2nreurex  27422  dirith2  27506  selberg2lem  27528  qabvle  27603  qabvexp  27604  ostth  27617  noextendseq  27646  noetasuplem4  27715  noetainflem4  27719  scutun12  27789  madebdayim  27860  addsrid  27927  addsfo  27946  peano2no  27947  negscl  27994  subsfo  28021  subsid1  28024  muls01  28062  mulsrid  28063  divs1  28153  recsex  28167  abssnid  28187  noseqp1  28214  noseqind  28215  peano2nns  28268  istrkg2ld  28336  istrkg3ld  28337  ttgval  28751  ttgvalOLD  28752  cchhllemOLD  28770  brbtwn  28782  colinearalglem4  28792  upgr0eop  28999  uspgrushgr  29062  usgruspgr  29065  usgr0eop  29131  0grsubgr  29163  uspgrloopvtx  29401  umgr2v2evtx  29407  usgr0edg0rusgr  29461  rgrusgrprc  29475  wlkvtxiedg  29511  pthdivtx  29615  usgr2pthlem  29649  wlkswwlksf1o  29762  wwlksext2clwwlk  29939  konigsbergssiedgw  30132  frgrncvvdeqlem7  30187  2clwwlk2  30230  ex-po  30317  pliguhgr  30368  nvnd  30570  ipval2lem3  30587  ipval2  30589  ipidsq  30592  dipcj  30596  dip0r  30599  nmlnogt0  30679  blocni  30687  ipasslem2  30714  ipasslem8  30719  ipasslem9  30720  ajval  30743  ubthlem1  30752  hvaddlid  30905  hvsub0  30958  hi02  30979  hlimi  31070  isch2  31105  chlimi  31116  chsupunss  31226  shsupunss  31228  chlejb1i  31358  h1dei  31432  h1de2ci  31438  spanunsni  31461  pjoml2i  31467  pjorthi  31551  mayete3i  31610  hosubid1  31680  nmopge0  31793  nmfnge0  31809  adj1  31815  adjeq  31817  lnop0  31848  lnopmi  31882  nmophmi  31913  cnlnadjlem5  31953  cnlnadjeui  31959  unierri  31986  leoprf2  32009  leopnmid  32020  nmopleid  32021  hstles  32113  hst0  32115  strlem3a  32134  dmdbr2  32185  mdsl1i  32203  mdsl2i  32204  mdsl2bi  32205  cvmdi  32206  mdslmd1lem1  32207  mdslmd1lem2  32208  mdslmd1i  32211  mdslmd2i  32212  csmdsymi  32216  mdexchi  32217  superpos  32236  atomli  32264  atordi  32266  chirredlem1  32272  chirredlem2  32273  atcvat4i  32279  atabsi  32283  mdsymlem1  32285  mdsymlem5  32289  mdsymlem6  32290  sumdmdii  32297  dmdbr5ati  32304  dmdbr6ati  32305  mddmdin0i  32313  cdj3lem2  32317  unidifsnel  32410  unidifsnne  32411  xppreima  32513  abfmpunirn  32519  abfmpel  32522  aciunf1lem  32529  fgreu  32539  imafi2  32575  padct  32583  fpwrelmapffslem  32596  fpwrelmap  32597  xrge0infss  32612  xrdifh  32630  pfx1s2  32749  clatp0cl  32792  clatp1cl  32793  cntrcrng  32866  cycpmco2lem4  32942  rmfsupp2  33038  1fldgenq  33108  resvval  33137  rearchi  33157  qusxpid  33174  opprabs  33294  zringfrac  33366  rlmdim  33435  locfinreflem  33569  locfinref  33570  ordtconnlem1  33653  rge0scvg  33678  lmxrge0  33681  qqh0  33713  qqh1  33714  rrh0  33744  zrhre  33748  esumcst  33810  esumfzf  33816  esumfsupre  33818  hasheuni  33832  sgon  33871  dmvlsiga  33876  sigainb  33883  measval  33945  ismeas  33946  sxbrsigalem0  34019  omssubadd  34048  carsggect  34066  eulerpartlemmf  34123  eulerpartlemgs2  34128  eulerpartlemn  34129  rrvsum  34202  ballotlem2  34236  ballotlemfcc  34241  ballotlem4  34246  signsplypnf  34310  signsply0  34311  signsw0glem  34313  signswrid  34318  signlem0  34347  signshf  34348  bnj535  34649  bnj580  34672  bnj907  34726  bnj1253  34776  funen1cnv  34839  loop1cycl  34875  ptpconn  34971  cvmsss2  35012  cvmlift2lem12  35052  cvmlift2lem13  35053  cvmliftphtlem  35055  cvmliftpht  35056  fmlafvel  35123  mppsthm  35317  bcneg1  35458  fv1stcnv  35500  fv2ndcnv  35501  wlimeq1  35544  imagesset  35677  altopeq1  35687  brcolinear2  35782  cldbnd  35938  ivthALT  35947  refssfne  35970  ontgval  36043  onint1  36061  axc11n11r  36288  bj-pm11.53a  36383  bj-bm1.3ii  36671  bj-restsn0  36692  bj-restsn10  36693  bj-restsnid  36694  bj-rest10  36695  bj-rest0  36700  bj-inftyexpiinv  36815  bj-inftyexpidisj  36817  taupilem1  36928  irrdiff  36933  f1omptsnlem  36943  mptsnunlem  36945  topdifinffinlem  36954  inunissunidif  36982  rdgssun  36985  exrecfnlem  36986  exrecfnpw  36988  finixpnum  37206  tan2h  37213  matunitlindflem2  37218  ptrest  37220  poimirlem22  37243  poimirlem25  37246  mblfinlem1  37258  mblfinlem2  37259  mblfinlem3  37260  mblfinlem4  37261  ismblfin  37262  itg2addnclem  37272  itg2addnclem2  37273  itg2addnclem3  37274  itg2addnc  37275  itg2gt0cn  37276  ftc1anclem5  37298  ftc1anclem8  37301  dvasin  37305  dvacos  37306  sdclem2  37343  totbndbnd  37390  heibor1lem  37410  heiborlem7  37418  bfplem1  37423  prnc  37668  ecexALTV  37930  brxrn  37973  riotasv  38558  glbconN  38976  glbconNOLD  38977  atpointN  39343  polsubN  39507  pol0N  39509  pol1N  39510  2polvalN  39514  2polssN  39515  3polN  39516  pcl0N  39522  2pmaplubN  39526  pnonsingN  39533  polsubclN  39552  cdlemefs32sn1aw  40014  cdleme43fsv1snlem  40020  cdleme41sn3a  40033  cdleme32a  40041  cdleme40m  40067  cdleme40n  40068  cdleme42b  40078  istendo  40360  cdlemk40  40517  cdlemkid  40536  dihvalcqpre  40835  facp2  41743  fac2xp3  41822  2xp3dxp2ge1d  41824  factwoffsmonot  41825  fnsnbt  41851  frlmsnic  41905  relt0neg1  42131  sn-nnne0  42135  sn-inelr  42152  prjspnerlem  42173  prjspnval2  42174  0prjspn  42184  3cubes  42249  mapfzcons1cl  42277  eldioph3b  42324  eldiophss  42333  0dioph  42337  vdioph  42338  eldioph4b  42370  eldioph4i  42371  rencldnfilem  42379  rmxy1  42482  rmxy0  42483  rmxm1  42494  rmym1  42495  monotoddzzfi  42502  wepwso  42606  aomclem6  42622  pwslnmlem0  42654  isnumbasabl  42669  areaquad  42783  onexlimgt  42810  oaabsb  42862  nadd1suc  42960  om2  42973  oe2  42975  safesnsupfidom1o  42986  onno  43002  oa1cl  43016  finona1cl  43022  reabsifneg  43201  reabsifnneg  43204  relexp2  43246  eltrclrec  43249  elrtrclrec  43250  brtrclrec  43265  brrtrclrec  43266  relexpxpmin  43286  dftrcl3  43289  dfrtrcl3  43302  heeq1  43346  seff  43885  lhe4.4ex1a  43905  eelT0  44353  snssl  44408  sineq0ALT  44515  elrnmpt1sf  44698  founiiun0  44699  supxrgere  44850  supxrgelem  44854  fmuldfeqlem1  45105  fmuldfeq  45106  climneg  45133  sumnnodd  45153  liminfltlem  45327  xlimpnfxnegmnf2  45381  addccncf2  45399  dvsinax  45436  stoweidlem18  45541  stoweidlem19  45542  stoweidlem22  45545  stoweidlem34  45557  stoweidlem40  45563  stoweidlem41  45564  stoweidlem55  45578  stoweidlem59  45582  dirker2re  45615  dirkerdenne0  45616  fourierdlem48  45677  fourierdlem49  45678  fourierdlem70  45699  fourierdlem71  45700  fourierdlem104  45733  fourierdlem112  45741  fouriersw  45754  etransclem46  45803  etransclem48  45805  nnfoctbdjlem  45978  natlocalincr  46397  singoutnword  46403  upwrdfi  46408  sqrtnegnre  46822  fsummmodsnunz  46849  flsqrt5  47068  bits0ALTV  47153  mogoldbblem  47194  sgoldbeven3prm  47257  nnsum3primes4  47262  isubgr0uhgr  47340  ushggricedg  47376  2zrngnmlid  47500  2zrngnmrid  47501  mpoexxg2  47584  lco0  47678  zlmodzxzldeplem3  47753  0dig1  47865  naryfvalel  47886  ackvalsuc0val  47943  aacllem  48417