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  3444  elabg  3634  eueq2  3672  sbcgf  3815  sbcralg  3828  csbconstgf  3871  sbcnestgw  4376  csbnestgw  4377  sbcnestg  4381  csbnestg  4382  csbnest1g  4385  iinexg  5290  eusv2nf  5337  reusv2lem5  5344  nnullss  5409  xpss1  5642  xpiindi  5782  reldm0  5874  elrnmpt1s  5905  resdm  5981  eliniseg  6049  trinxp  6078  ssrnres  6131  cnveq0  6150  coi2  6216  relrelss  6225  cnviin  6238  elpred  6270  onelssex  6360  ord0eln0  6367  funcnvres  6564  funimaex  6574  fnresin1  6611  fnresin2  6612  fresin  6697  ssimaex  6912  fvmpt  6934  fvmptnf  6956  fvimacnvALT  6995  dff3  7038  fsn  7073  fsn2  7074  funop  7087  fvrnressn  7099  fnsnbg  7104  fninfp  7114  fndifnfp  7116  fnnfpeq0  7118  fprb  7134  elabrex  7182  elabrexg  7183  f1elima  7204  f1ofvswap  7247  fliftel1  7251  f1owe  7294  sorpssuni  7672  sorpssint  7673  eldifpw  7708  ordeleqon  7722  ordsson  7723  ssnlim  7826  abrexexg  7903  tposfun  8182  tpostpos2  8187  fpr3g  8225  wfr3g  8259  tfrlem10  8316  tfrlem12  8318  tfr3  8328  seqomlem1  8379  seqomlem2  8380  seqomlem4  8382  ondif2  8427  oa0  8441  om0  8442  oa1suc  8456  om1  8467  oe1  8469  oe1m  8470  omass  8505  oeoalem  8521  oeoelem  8523  nnmsucr  8550  nnm1  8577  nnm2  8578  naddrid  8608  naddlid  8609  ecelqs  8702  xpider  8722  mapdm0  8776  fvdiagfn  8825  ixpsnf1o  8872  xp1en  8987  undom  8989  sbthlem7  9017  domunsn  9051  xpmapenlem  9068  infensuc  9079  findcard2d  9090  diffi  9099  cnvfi  9100  enreffi  9107  snnen2o  9144  1sdom2dom  9153  infi  9171  finresfin  9173  unblem1  9197  unblem2  9198  unblem3  9199  unblem4  9200  isfinite2  9203  infn0ALT  9210  unfilem1  9212  unfilem2  9213  unfir  9215  fofinf1o  9241  cnvfiALT  9248  mptfi  9260  finsschain  9268  marypha2  9348  inf0  9536  trcl  9643  frr3g  9671  r1rankidb  9719  snwf  9724  unwf  9725  uniwf  9734  rankval3b  9741  rankr1a  9751  rankxplim3  9796  scott0  9801  djueq1  9820  card1  9883  pm54.43  9916  infxpenc2  9935  dfac8clem  9945  alephsuc2  9993  alephle  10001  cardaleph  10002  dfac12lem2  10058  undjudom  10081  djudom1  10096  pwdju1  10104  nnadju  10111  ackbij1lem18  10149  cflem  10158  cflemOLD  10159  cflecard  10166  cfeq0  10169  cfslb  10179  cfsmolem  10183  cfcoflem  10185  cfidm  10188  isfin4p1  10228  fin23lem12  10244  fin23lem16  10248  fin23lem28  10253  fin23lem38  10262  fin23lem41  10265  fin1a2lem7  10319  fin1a2lem12  10324  fin1a2lem13  10325  hsmexlem8  10337  axcc2lem  10349  axcc3  10351  domtriomlem  10355  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  ac6num  10392  ttukeylem4  10425  ttukeylem7  10428  ttukey2g  10429  axdclem  10432  brdom3  10441  brdom5  10442  cardeq0  10465  unsnen  10466  konigthlem  10481  pwcfsdom  10496  canthp1lem1  10565  wunex2  10651  wuncval2  10660  eltsk2g  10664  ingru  10728  grutsk  10735  axgroth6  10741  mulidpi  10799  nlt1pi  10819  indpi  10820  pinq  10840  mulidnq  10876  1idpr  10942  prlem934  10946  0idsr  11010  1idsr  11011  00sr  11012  negexsr  11015  recexsrlem  11016  sqgt0sr  11019  ax1rid  11074  axcnre  11077  ne0gt0  11239  peano2cn  11306  peano2re  11307  00id  11309  mul02lem2  11311  mul01  11313  subid  11401  subid1  11402  negid  11429  negeq0  11436  peano2cnm  11448  peano2rem  11449  lt0neg1  11644  le0neg1  11646  relin01  11662  div2neg  11865  recgt0ii  12049  divgt0i2i  12058  ledivp1i  12068  ltdivp1i  12069  inelr  12136  peano5nni  12149  peano2nn  12158  nnge1  12174  nnne0  12180  times2  12278  addltmul  12378  nn0p1nn  12441  peano2nn0  12442  nn0lele2xi  12458  fcdmnn0supp  12459  fcdmnn0fsupp  12460  fcdmnn0suppg  12461  peano2z  12534  peano2zm  12536  suprzcl  12574  zeo  12580  eluzaddi  12784  uzwo  12830  uzwo2  12831  infssuzle  12850  infssuzcl  12851  zq  12873  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  rphalfcl  12940  zgt1rpn0n1  12954  ltpnf  13040  nltmnf  13049  pnfge  13050  nltpnft  13084  xlemnf  13087  qsqueeze  13121  xlt0neg1  13139  xle0neg1  13141  xaddpnf1  13146  xaddmnf1  13148  xaddrid  13161  xsubge0  13181  xmul01  13187  xmulneg1  13189  xmulpnf1  13194  xmulrid  13199  supxrbnd  13248  supxrgtmnf  13249  supxrre1  13250  supxrre2  13251  elioopnf  13364  elicopnf  13366  iccshftri  13408  iccshftli  13410  iccdili  13412  icccntri  13414  fzprval  13506  fz0add1fz1  13656  fzofzp1  13685  fzostep1  13704  injresinj  13709  flge0nn0  13742  flge1nn  13743  btwnzge0  13750  modfrac  13806  om2uzsuci  13873  axdc4uzlem  13908  ser1const  13983  exp0  13990  exp1  13992  expn1  13996  nn0sqcl  14014  sqval  14039  sqeq0  14045  resqcl  14049  zsqcl  14054  expubnd  14103  binom21  14144  expnbnd  14157  nn0opthlem2  14194  bcnn  14237  bcn2  14244  bcn2p1  14250  bcnm1  14252  hasheq0  14288  hashsng  14294  hashen1  14295  hashunsnggt  14319  hashin  14336  hashdif  14338  hashgt23el  14349  hashxplem  14358  hashf1lem2  14381  hash2pr  14394  hash2prde  14395  pr2pwpr  14404  hash3tr  14416  iswrd  14440  wrdval  14441  hashwrdn  14472  ccatval2  14503  ccatrid  14512  eqs1  14537  s111  14540  ccatws1len  14545  repsw0  14701  repsw1  14707  cshw0  14718  wwlktovf  14881  relexpsucnnl  14955  reim0  15043  imval2  15076  cjne0  15088  abssq  15231  max0add  15235  abs2dif  15258  rddif  15266  absrdbnd  15267  rexuz3  15274  isershft  15589  isercolllem2  15591  isercoll  15593  fsum  15645  fsumadd  15665  fsumsplitsnun  15680  bcxmas  15760  infcvgaux2i  15783  fprod  15866  risefac0  15952  fallfac0  15953  risefac1  15958  fallfac1  15959  bpoly2  15982  bpoly3  15983  bpoly4  15984  fsumcube  15985  efi4p  16064  resin4p  16065  recos4p  16066  sinbnd  16107  cosbnd  16108  rpnnen2lem8  16148  rpnnen2lem12  16152  cnso  16174  dvdsmul2  16207  dvdslelem  16238  odd2np1lem  16269  mod2eq1n2dvds  16276  divalglem0  16322  divalglem1  16323  divalglem4  16325  divalglem5  16326  divalglem8  16329  flodddiv4  16344  bits0  16357  bitsp1o  16362  bitsf1  16375  sadadd2lem2  16379  gcd1  16457  lcm0val  16523  dvdslcm  16527  lcmeq0  16529  lcmgcd  16536  lcm1  16539  lcmfunsnlem2lem2  16568  lcmfunsnlem2  16569  prm2orodd  16620  phiprm  16706  pc0  16784  pcdvdstr  16806  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  hashbc0  16935  setsval  17096  fsets  17098  setsres  17107  ressinbas  17174  ressress  17176  elrestr  17350  pwssnf1o  17420  xpsfrnel  17484  xpscf  17487  ismred2  17523  submre  17525  mreacs  17582  oppchomfval  17638  brssc  17739  isssc  17745  yonedalem4c  18201  oduleval  18213  isprs  18220  oduclatb  18431  gsumval2a  18577  smndex1n0mnd  18804  mulg1  18978  mulgnegnn  18981  isghmOLD  19113  ghmghmrn  19132  cntrnsg  19241  oppgplusfval  19245  pgrpsubgsymg  19306  psgneldm2i  19402  efgrelexlemb  19647  frgp0  19657  frgpmhm  19662  vrgpf  19665  cntrcmnd  19739  cntrabl  19740  cygctb  19789  dprd0  19930  dprd2da  19941  mgpplusg  20047  opprmulfval  20242  subrngint  20463  subrgint  20498  lsp0  20930  rlmval2  21114  cncrng  21313  cnfld1  21318  zringcyg  21394  mulgrhm2  21403  zlmsca  21445  fermltlchr  21454  chrnzr  21455  zrhpsgnelbas  21519  ocvz  21603  cssincl  21613  css0  21614  css1  21615  frlmip  21703  fczpsrbag  21846  ply1idvr1OLD  22198  evls1rhmlem  22224  evl1fval1lem  22233  marrepeval  22466  decpmatid  22673  0opn  22807  topopn  22809  basdif0  22856  tgval  22858  isopn2  22935  0cld  22941  ntropn  22952  ntrval2  22954  ntrdif  22955  clsdif  22956  cmclsopn  22965  ntrtop  22973  ntr0  22984  mretopd  22995  neips  23016  neiptopnei  23035  maxlp  23050  isperf2  23055  rest0  23072  iocpnfordt  23118  icomnfordt  23119  mnfnei  23124  refref  23416  unisngl  23430  1stckgen  23457  ptbasfi  23484  pthaus  23541  fbssfi  23740  isfil2  23759  ssfg  23775  filconn  23786  fbasrn  23787  filufint  23823  imaelfm  23854  fmfnfmlem4  23860  fclsfnflim  23930  alexsubALTlem3  23952  alexsubALTlem4  23953  ustfilxp  24116  ustuqtop2  24146  ustuqtop4  24148  utopsnneiplem  24151  utopsnnei  24153  utop2nei  24154  cfiluweak  24198  neipcfilu  24199  xmetres  24268  metres  24269  mopnex  24423  prdsms  24435  metucn  24475  tngds  24552  tngngp3  24560  nmoge0  24625  cnfldnm  24682  tgioo  24700  xrtgioo  24711  xrsmopn  24717  negcncf  24831  negcncfOLD  24832  phtpy01  24900  pco0  24930  tcphtopn  25142  tchnmfval  25144  caussi  25213  rrxip  25306  minveclem3b  25344  ovolfioo  25384  ovolficc  25385  ovolfsf  25388  ovolctb  25407  ovolctb2  25409  ovolfiniun  25418  ovoliun2  25423  ovolshftlem1  25426  ovolscalem1  25430  ovolicopnf  25441  iunmbl2  25474  uniioombllem2  25500  opnmblALT  25520  ismbf  25545  mbfinf  25582  0plef  25589  itg1climres  25631  itg2cnlem1  25678  iblitg  25685  ibl0  25704  itgcn  25762  cnlimc  25805  dvfre  25871  dvnfre  25872  dveflem  25899  dvef  25900  dvlipcn  25915  lhop2  25936  itgsubstlem  25971  deg1val  26017  ply1rem  26087  coefv0  26169  plyrecj  26203  vieta1lem2  26235  aannenlem1  26252  aaliou2b  26265  ulmval  26305  ulmpm  26308  ulmdvlem1  26325  mtest  26329  efcn  26369  sin2pim  26410  cos2pim  26411  sinmpi  26412  cosmpi  26413  sinppi  26414  cosppi  26415  efimpi  26416  sincosq1lem  26422  sincosq2sgn  26424  sincosq3sgn  26425  sincosq4sgn  26426  sinq12gt0  26432  sinq34lt0t  26434  sincosq1eq  26437  abssinper  26446  efif1o  26471  loglt1b  26559  relogcn  26563  ellogdm  26564  efopn  26583  cxp0  26595  cxp1  26596  cxpsqrt  26628  logsqrt  26629  logb1  26695  atandm3  26804  atanbnd  26852  atancn  26862  leibpi  26868  efrlim  26895  efrlimOLD  26896  logdifbnd  26920  vmaprm  27043  ppip1le  27087  ppieq0  27102  prmorcht  27104  ppiublem1  27129  ppiub  27131  chpeq0  27135  chtub  27139  fsumvma  27140  pclogsum  27142  chpval2  27145  dchrresb  27186  dchrptlem1  27191  lgs0  27237  lgs2  27241  lgsdir2lem2  27253  lgsdir2lem4  27255  lgsdchrval  27281  lgsdchr  27282  lgseisenlem2  27303  2lgslem1c  27320  2lgsoddprmlem2  27336  addsq2nreurex  27371  dirith2  27455  selberg2lem  27477  qabvle  27552  qabvexp  27553  ostth  27566  noextendseq  27595  noetasuplem4  27664  noetainflem4  27668  scutun12  27739  madebdayim  27820  bdayiun  27847  addsrid  27894  addsfo  27913  peano2no  27914  negscl  27965  subsfo  27992  subsid1  27995  muls01  28038  mulsrid  28039  divs1  28130  recsex  28144  abssnid  28168  peano2ons  28199  noseqp1  28208  noseqind  28209  peano2nns  28265  n0sfincut  28269  dfnns2  28284  elzs2  28310  elnnzs  28312  elznns  28313  zsoring  28319  n0seo  28331  exps0  28337  exps1  28338  istrkg2ld  28423  istrkg3ld  28424  ttgval  28838  brbtwn  28862  colinearalglem4  28872  upgr0eop  29077  uspgrushgr  29140  usgruspgr  29143  usgr0eop  29209  0grsubgr  29241  uspgrloopvtx  29479  umgr2v2evtx  29485  usgr0edg0rusgr  29539  rgrusgrprc  29553  wlkvtxiedg  29588  pthdivtx  29690  usgr2pthlem  29726  wlkswwlksf1o  29842  wwlksext2clwwlk  30019  konigsbergssiedgw  30212  frgrncvvdeqlem7  30267  2clwwlk2  30310  ex-po  30397  pliguhgr  30448  nvnd  30650  ipval2lem3  30667  ipval2  30669  ipidsq  30672  dipcj  30676  dip0r  30679  nmlnogt0  30759  blocni  30767  ipasslem2  30794  ipasslem8  30799  ipasslem9  30800  ajval  30823  ubthlem1  30832  hvaddlid  30985  hvsub0  31038  hi02  31059  hlimi  31150  isch2  31185  chlimi  31196  chsupunss  31306  shsupunss  31308  chlejb1i  31438  h1dei  31512  h1de2ci  31518  spanunsni  31541  pjoml2i  31547  pjorthi  31631  mayete3i  31690  hosubid1  31760  nmopge0  31873  nmfnge0  31889  adj1  31895  adjeq  31897  lnop0  31928  lnopmi  31962  nmophmi  31993  cnlnadjlem5  32033  cnlnadjeui  32039  unierri  32066  leoprf2  32089  leopnmid  32100  nmopleid  32101  hstles  32193  hst0  32195  strlem3a  32214  dmdbr2  32265  mdsl1i  32283  mdsl2i  32284  mdsl2bi  32285  cvmdi  32286  mdslmd1lem1  32287  mdslmd1lem2  32288  mdslmd1i  32291  mdslmd2i  32292  csmdsymi  32296  mdexchi  32297  superpos  32316  atomli  32344  atordi  32346  chirredlem1  32352  chirredlem2  32353  atcvat4i  32359  atabsi  32363  mdsymlem1  32365  mdsymlem5  32369  mdsymlem6  32370  sumdmdii  32377  dmdbr5ati  32384  dmdbr6ati  32385  mddmdin0i  32393  cdj3lem2  32397  unidifsnel  32497  unidifsnne  32498  xppreima  32602  abfmpunirn  32609  abfmpel  32612  aciunf1lem  32619  fgreu  32629  imafi2  32668  padct  32676  fpwrelmapffslem  32688  fpwrelmap  32689  xrge0infss  32716  xrdifh  32736  pfx1s2  32893  clatp0cl  32931  clatp1cl  32932  cntrcrng  33036  cycpmco2lem4  33084  rmfsupp2  33191  1fldgenq  33274  resvval  33280  rearchi  33296  qusxpid  33313  opprabs  33432  zringfrac  33504  rlmdim  33584  constrfiss  33720  2sqr3minply  33749  locfinreflem  33809  locfinref  33810  ordtconnlem1  33893  rge0scvg  33918  lmxrge0  33921  qqh0  33953  qqh1  33954  rrh0  33984  zrhre  33988  esumcst  34032  esumfzf  34038  esumfsupre  34040  hasheuni  34054  sgon  34093  dmvlsiga  34098  sigainb  34105  measval  34167  ismeas  34168  sxbrsigalem0  34241  omssubadd  34270  carsggect  34288  eulerpartlemmf  34345  eulerpartlemgs2  34350  eulerpartlemn  34351  rrvsum  34424  ballotlem2  34459  ballotlemfcc  34464  ballotlem4  34469  signsplypnf  34520  signsply0  34521  signsw0glem  34523  signswrid  34528  signlem0  34557  signshf  34558  bnj535  34859  bnj580  34882  bnj907  34936  bnj1253  34986  funen1cnv  35057  onvf1odlem1  35078  onvf1od  35082  loop1cycl  35112  ptpconn  35208  cvmsss2  35249  cvmlift2lem12  35289  cvmlift2lem13  35290  cvmliftphtlem  35292  cvmliftpht  35293  fmlafvel  35360  mppsthm  35554  bcneg1  35711  fv1stcnv  35752  fv2ndcnv  35753  wlimeq1  35796  imagesset  35929  altopeq1  35939  brcolinear2  36034  cldbnd  36302  ivthALT  36311  refssfne  36334  ontgval  36407  onint1  36425  axc11n11r  36659  bj-pm11.53a  36754  bj-bm1.3ii  37040  bj-restsn0  37061  bj-restsn10  37062  bj-restsnid  37063  bj-rest10  37064  bj-rest0  37069  bj-inftyexpiinv  37184  bj-inftyexpidisj  37186  taupilem1  37297  irrdiff  37302  f1omptsnlem  37312  mptsnunlem  37314  topdifinffinlem  37323  inunissunidif  37351  rdgssun  37354  exrecfnlem  37355  exrecfnpw  37357  finixpnum  37587  tan2h  37594  matunitlindflem2  37599  ptrest  37601  poimirlem22  37624  poimirlem25  37627  mblfinlem1  37639  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  ismblfin  37643  itg2addnclem  37653  itg2addnclem2  37654  itg2addnclem3  37655  itg2addnc  37656  itg2gt0cn  37657  ftc1anclem5  37679  ftc1anclem8  37682  dvasin  37686  dvacos  37687  sdclem2  37724  totbndbnd  37771  heibor1lem  37791  heiborlem7  37799  bfplem1  37804  prnc  38049  brxrn  38344  riotasv  38940  glbconN  39358  glbconNOLD  39359  atpointN  39725  polsubN  39889  pol0N  39891  pol1N  39892  2polvalN  39896  2polssN  39897  3polN  39898  pcl0N  39904  2pmaplubN  39908  pnonsingN  39915  polsubclN  39934  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme41sn3a  40415  cdleme32a  40423  cdleme40m  40449  cdleme40n  40450  cdleme42b  40460  istendo  40742  cdlemk40  40899  cdlemkid  40918  dihvalcqpre  41217  facp2  42119  relt0neg1  42432  sn-nnne0  42436  frlmsnic  42516  prjspnerlem  42593  prjspnval2  42594  0prjspn  42604  3cubes  42666  mapfzcons1cl  42694  eldioph3b  42741  eldiophss  42750  0dioph  42754  vdioph  42755  eldioph4b  42787  eldioph4i  42788  rencldnfilem  42796  rmxy1  42898  rmxy0  42899  rmxm1  42910  rmym1  42911  monotoddzzfi  42918  wepwso  43019  aomclem6  43035  pwslnmlem0  43067  isnumbasabl  43082  areaquad  43192  onexlimgt  43219  oaabsb  43270  nadd1suc  43368  om2  43380  oe2  43382  safesnsupfidom1o  43393  onno  43409  oa1cl  43423  finona1cl  43429  reabsifneg  43608  reabsifnneg  43611  relexp2  43653  eltrclrec  43656  elrtrclrec  43657  brtrclrec  43672  brrtrclrec  43673  relexpxpmin  43693  dftrcl3  43696  dfrtrcl3  43709  heeq1  43753  seff  44285  lhe4.4ex1a  44305  eelT0  44751  snssl  44806  sineq0ALT  44913  trfr  44939  xpwf  44941  dmwf  44942  rnwf  44943  modelaxreplem1  44955  modelaxreplem3  44957  0elaxnul  44960  prclaxpr  44962  uniclaxun  44963  wfac8prim  44979  permaxinf2lem  44989  elrnmpt1sf  45170  founiiun0  45171  supxrgere  45316  supxrgelem  45320  fmuldfeqlem1  45567  fmuldfeq  45568  climneg  45595  sumnnodd  45615  liminfltlem  45789  xlimpnfxnegmnf2  45843  addccncf2  45861  dvsinax  45898  stoweidlem18  46003  stoweidlem19  46004  stoweidlem22  46007  stoweidlem34  46019  stoweidlem40  46025  stoweidlem41  46026  stoweidlem55  46040  stoweidlem59  46044  dirker2re  46077  dirkerdenne0  46078  fourierdlem48  46139  fourierdlem49  46140  fourierdlem70  46161  fourierdlem71  46162  fourierdlem104  46195  fourierdlem112  46203  fouriersw  46216  etransclem46  46265  etransclem48  46267  nnfoctbdjlem  46440  ormklocald  46859  natlocalincr  46861  singoutnword  46867  cjnpoly  46877  sinnpoly  46879  sqrtnegnre  47295  fsummmodsnunz  47363  flsqrt5  47582  bits0ALTV  47667  mogoldbblem  47708  sgoldbeven3prm  47771  nnsum3primes4  47776  isubgr0uhgr  47861  ushggricedg  47915  2zrngnmlid  48243  2zrngnmrid  48244  mpoexxg2  48326  lco0  48416  zlmodzxzldeplem3  48491  0dig1  48598  naryfvalel  48619  ackvalsuc0val  48676  iinxp  48819  0funclem  49075  aacllem  49790