Theorem mpan2 690

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mpanr12  704  mp3an23  1454  elvd  3482  eueq2  3706  sbcgf  3854  sbcralg  3868  csbconstgf  3911  sbcnestgw  4420  csbnestgw  4421  sbcnestg  4425  csbnestg  4426  csbnest1g  4429  mpteq1OLD  5242  iinexg  5341  eusv2nf  5393  reusv2lem5  5400  nnullss  5462  xpss1  5695  xpiindi  5834  reldm0  5926  elrnmpt1s  5955  resdm  6025  eliniseg  6091  trinxp  6124  ssrnres  6175  cnveq0  6194  coi2  6260  relrelss  6270  cnviin  6283  elpred  6315  onelssex  6410  ord0eln0  6417  funcnvres  6624  funimaex  6634  fnresin1  6673  fnresin2  6674  fresin  6758  ssimaex  6974  fvmpt  6996  fvmptnf  7018  fvimacnvALT  7056  dff3  7099  fsn  7130  fsn2  7131  funop  7144  fvrnressn  7156  fninfp  7169  fndifnfp  7171  fnnfpeq0  7173  fprb  7192  elabrex  7239  f1elima  7259  f1ofvswap  7301  fliftel1  7304  f1owe  7347  sorpssuni  7719  sorpssint  7720  eldifpw  7752  ordeleqon  7766  ordsson  7767  ssnlim  7872  abrexexg  7944  tposfun  8224  tpostpos2  8229  fpr3g  8267  wfr3g  8304  wfrlem14OLD  8319  wfrlem15OLD  8320  tfrlem10  8384  tfrlem12  8386  tfr3  8396  seqomlem1  8447  seqomlem2  8448  seqomlem4  8450  ondif2  8499  oa0  8513  om0  8514  oa1suc  8528  om1  8539  oe1  8541  oe1m  8542  omass  8577  oeoalem  8593  oeoelem  8595  nnmsucr  8622  nnm1  8648  nnm2  8649  naddrid  8679  naddlid  8680  ecelqsg  8763  xpider  8779  mapdm0  8833  fvdiagfn  8882  ixpsnf1o  8929  xp1en  9054  undom  9056  sbthlem7  9086  domunsn  9124  xpmapenlem  9141  infensuc  9152  findcard2d  9163  diffi  9176  cnvfi  9177  enreffi  9183  snnen2o  9234  1sdom2dom  9244  infi  9265  finresfin  9267  unblem1  9292  unblem2  9293  unblem3  9294  unblem4  9295  isfinite2  9298  infn0ALT  9305  unfilem1  9307  unfilem2  9308  unfir  9311  fofinf1o  9324  cnvfiALT  9331  pwfilemOLD  9343  mptfi  9348  finsschain  9356  marypha2  9431  inf0  9613  trcl  9720  frr3g  9748  r1rankidb  9796  snwf  9801  unwf  9802  uniwf  9811  rankval3b  9818  rankr1a  9828  rankxplim3  9873  scott0  9878  djueq1  9897  card1  9960  pm54.43  9993  infxpenc2  10014  dfac8clem  10024  alephsuc2  10072  alephle  10080  cardaleph  10081  dfac12lem2  10136  undjudom  10159  djudom1  10174  pwdju1  10182  nnadju  10189  ackbij1lem18  10229  cflem  10238  cflecard  10245  cfeq0  10248  cfslb  10258  cfsmolem  10262  cfcoflem  10264  cfidm  10267  isfin4p1  10307  fin23lem12  10323  fin23lem16  10327  fin23lem28  10332  fin23lem38  10341  fin23lem41  10344  fin1a2lem7  10398  fin1a2lem12  10403  fin1a2lem13  10404  hsmexlem8  10416  axcc2lem  10428  axcc3  10430  domtriomlem  10434  axdc3lem2  10443  axdc3lem4  10445  axdc4lem  10447  axcclem  10449  ac6num  10471  ttukeylem4  10504  ttukeylem7  10507  ttukey2g  10508  axdclem  10511  brdom3  10520  brdom5  10521  cardeq0  10544  unsnen  10545  konigthlem  10560  pwcfsdom  10575  canthp1lem1  10644  wunex2  10730  wuncval2  10739  eltsk2g  10743  ingru  10807  grutsk  10814  axgroth6  10820  mulidpi  10878  nlt1pi  10898  indpi  10899  pinq  10919  mulidnq  10955  1idpr  11021  prlem934  11025  0idsr  11089  1idsr  11090  00sr  11091  negexsr  11094  recexsrlem  11095  sqgt0sr  11098  ax1rid  11153  axcnre  11156  ne0gt0  11316  peano2cn  11383  peano2re  11384  00id  11386  mul02lem2  11388  mul01  11390  subid  11476  subid1  11477  negid  11504  negeq0  11511  peano2cnm  11523  peano2rem  11524  lt0neg1  11717  le0neg1  11719  relin01  11735  div2neg  11934  recgt0ii  12117  divgt0i2i  12126  ledivp1i  12136  ltdivp1i  12137  peano5nni  12212  peano2nn  12221  nnge1  12237  nnne0  12243  times2  12346  addltmul  12445  nn0p1nn  12508  peano2nn0  12509  nn0lele2xi  12524  fcdmnn0supp  12525  fcdmnn0fsupp  12526  fcdmnn0suppg  12527  peano2z  12600  peano2zm  12602  suprzcl  12639  zeo  12645  eluzaddi  12850  uzwo  12892  uzwo2  12893  infssuzle  12912  infssuzcl  12913  zq  12935  rpnnen1lem1  12959  rpnnen1lem3  12960  rpnnen1lem5  12962  rphalfcl  12998  zgt1rpn0n1  13012  ltpnf  13097  nltmnf  13106  pnfge  13107  nltpnft  13140  xlemnf  13143  qsqueeze  13177  xlt0neg1  13195  xle0neg1  13197  xaddpnf1  13202  xaddmnf1  13204  xaddrid  13217  xsubge0  13237  xmul01  13243  xmulneg1  13245  xmulpnf1  13250  xmulrid  13255  supxrbnd  13304  supxrgtmnf  13305  supxrre1  13306  supxrre2  13307  elioopnf  13417  elicopnf  13419  iccshftri  13461  iccshftli  13463  iccdili  13465  icccntri  13467  fzprval  13559  fz0add1fz1  13699  fzofzp1  13726  fzostep1  13745  injresinj  13750  flge0nn0  13782  flge1nn  13783  btwnzge0  13790  modfrac  13846  om2uzsuci  13910  axdc4uzlem  13945  ser1const  14021  exp0  14028  exp1  14030  expn1  14034  nn0sqcl  14052  sqval  14077  sqeq0  14082  resqcl  14086  zsqcl  14091  expubnd  14139  binom21  14179  expnbnd  14192  nn0opthlem2  14226  bcnn  14269  bcn2  14276  bcn2p1  14282  bcnm1  14284  hasheq0  14320  hashsng  14326  hashen1  14327  hashunsnggt  14351  hashin  14368  hashdif  14370  hashgt23el  14381  hashxplem  14390  hashf1lem2  14414  hash2pr  14427  hash2prde  14428  pr2pwpr  14437  hash3tr  14448  iswrd  14463  wrdval  14464  hashwrdn  14494  ccatval2  14525  ccatrid  14534  eqs1  14559  s111  14562  ccatws1len  14567  repsw0  14724  repsw1  14730  cshw0  14741  wwlktovf  14904  relexpsucnnl  14974  reim0  15062  imval2  15095  cjne0  15107  abssq  15250  max0add  15254  abs2dif  15276  rddif  15284  absrdbnd  15285  rexuz3  15292  isershft  15607  isercolllem2  15609  isercoll  15611  fsum  15663  fsumadd  15683  fsumsplitsnun  15698  bcxmas  15778  infcvgaux2i  15801  fprod  15882  risefac0  15968  fallfac0  15969  risefac1  15974  fallfac1  15975  bpoly2  15998  bpoly3  15999  bpoly4  16000  fsumcube  16001  efi4p  16077  resin4p  16078  recos4p  16079  sinbnd  16120  cosbnd  16121  rpnnen2lem8  16161  rpnnen2lem12  16165  cnso  16187  dvdsmul2  16219  dvdslelem  16249  odd2np1lem  16280  mod2eq1n2dvds  16287  divalglem0  16333  divalglem1  16334  divalglem4  16336  divalglem5  16337  divalglem8  16340  flodddiv4  16353  bits0  16366  bitsp1o  16371  bitsf1  16384  sadadd2lem2  16388  gcd1  16466  lcm0val  16528  dvdslcm  16532  lcmeq0  16534  lcmgcd  16541  lcm1  16544  lcmfunsnlem2lem2  16573  lcmfunsnlem2  16574  prm2orodd  16625  phiprm  16707  pc0  16784  pcdvdstr  16806  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  hashbc0  16935  setsval  17097  fsets  17099  setsres  17108  ressinbas  17187  ressress  17190  elrestr  17371  pwssnf1o  17441  xpsfrnel  17505  xpscf  17508  ismred2  17544  submre  17546  mreacs  17599  oppchomfval  17655  oppchomfvalOLD  17656  brssc  17758  isssc  17764  yonedalem4c  18227  oduleval  18239  isprs  18247  oduclatb  18457  gsumval2a  18601  smndex1n0mnd  18790  mulg1  18956  mulgnegnn  18959  isghm  19087  ghmghmrn  19106  cntrnsg  19203  oppgplusfval  19207  pgrpsubgsymg  19272  psgneldm2i  19368  efgrelexlemb  19613  frgp0  19623  frgpmhm  19628  vrgpf  19631  cntrcmnd  19705  cntrabl  19706  cygctb  19755  dprd0  19896  dprd2da  19907  mgpplusg  19986  opprmulfval  20145  subrgint  20379  lsp0  20613  sralemOLD  20784  rlmval2  20809  zringcyg  21031  mulgrhm2  21040  zlmsca  21066  chrnzr  21074  zrhpsgnelbas  21139  ocvz  21223  cssincl  21233  css0  21234  css1  21235  frlmip  21325  fczpsrbag  21468  ply1idvr1  21809  evls1rhmlem  21832  evl1fval1lem  21841  marrepeval  22057  decpmatid  22264  0opn  22398  topopn  22400  basdif0  22448  tgval  22450  isopn2  22528  0cld  22534  ntropn  22545  ntrval2  22547  ntrdif  22548  clsdif  22549  cmclsopn  22558  ntrtop  22566  ntr0  22577  mretopd  22588  neips  22609  neiptopnei  22628  maxlp  22643  isperf2  22648  rest0  22665  iocpnfordt  22711  icomnfordt  22712  mnfnei  22717  refref  23009  unisngl  23023  1stckgen  23050  ptbasfi  23077  pthaus  23134  fbssfi  23333  isfil2  23352  ssfg  23368  filconn  23379  fbasrn  23380  filufint  23416  imaelfm  23447  fmfnfmlem4  23453  fclsfnflim  23523  alexsubALTlem3  23545  alexsubALTlem4  23546  ustfilxp  23709  ustuqtop2  23739  ustuqtop4  23741  utopsnneiplem  23744  utopsnnei  23746  utop2nei  23747  cfiluweak  23792  neipcfilu  23793  xmetres  23862  metres  23863  mopnex  24020  prdsms  24032  metucn  24072  tngds  24156  tngdsOLD  24157  tngngp3  24165  nmoge0  24230  cnfldnm  24287  tgioo  24304  xrtgioo  24314  xrsmopn  24320  negcncf  24430  phtpy01  24493  pco0  24522  tcphtopn  24735  tchnmfval  24737  caussi  24806  rrxip  24899  minveclem3b  24937  ovolfioo  24976  ovolficc  24977  ovolfsf  24980  ovolctb  24999  ovolctb2  25001  ovolfiniun  25010  ovoliun2  25015  ovolshftlem1  25018  ovolscalem1  25022  ovolicopnf  25033  iunmbl2  25066  uniioombllem2  25092  opnmblALT  25112  ismbf  25137  mbfinf  25174  0plef  25181  itg1climres  25224  itg2cnlem1  25271  iblitg  25278  ibl0  25296  itgcn  25354  cnlimc  25397  dvfre  25460  dvnfre  25461  dveflem  25488  dvef  25489  dvlipcn  25503  lhop2  25524  itgsubstlem  25557  deg1val  25606  ply1rem  25673  coefv0  25754  plyrecj  25785  vieta1lem2  25816  aannenlem1  25833  aaliou2b  25846  ulmval  25884  ulmpm  25887  ulmdvlem1  25904  mtest  25908  efcn  25947  sin2pim  25987  cos2pim  25988  sinmpi  25989  cosmpi  25990  sinppi  25991  cosppi  25992  efimpi  25993  sincosq1lem  25999  sincosq2sgn  26001  sincosq3sgn  26002  sincosq4sgn  26003  sinq12gt0  26009  sinq34lt0t  26011  sincosq1eq  26014  abssinper  26022  efif1o  26047  loglt1b  26134  relogcn  26138  ellogdm  26139  efopn  26158  cxp0  26170  cxp1  26171  cxpsqrt  26203  logsqrt  26204  logb1  26264  atandm3  26373  atanbnd  26421  atancn  26431  leibpi  26437  efrlim  26464  logdifbnd  26488  vmaprm  26611  ppip1le  26655  ppieq0  26670  prmorcht  26672  ppiublem1  26695  ppiub  26697  chpeq0  26701  chtub  26705  fsumvma  26706  pclogsum  26708  chpval2  26711  dchrresb  26752  dchrptlem1  26757  lgs0  26803  lgs2  26807  lgsdir2lem2  26819  lgsdir2lem4  26821  lgsdchrval  26847  lgsdchr  26848  lgseisenlem2  26869  2lgslem1c  26886  2lgsoddprmlem2  26902  addsq2nreurex  26937  dirith2  27021  selberg2lem  27043  qabvle  27118  qabvexp  27119  ostth  27132  noextendseq  27160  noetasuplem4  27229  noetainflem4  27233  scutun12  27301  madebdayim  27372  addsrid  27438  addsfo  27457  negscl  27500  subsid1  27526  muls01  27558  mulsrid  27559  divs1  27641  recsex  27655  istrkg2ld  27701  istrkg3ld  27702  ttgval  28116  ttgvalOLD  28117  cchhllemOLD  28135  brbtwn  28147  colinearalglem4  28157  upgr0eop  28364  uspgrushgr  28425  usgruspgr  28428  usgr0eop  28493  0grsubgr  28525  uspgrloopvtx  28762  umgr2v2evtx  28768  usgr0edg0rusgr  28822  rgrusgrprc  28836  wlkvtxiedg  28872  pthdivtx  28976  usgr2pthlem  29010  wlkswwlksf1o  29123  wwlksext2clwwlk  29300  konigsbergssiedgw  29493  frgrncvvdeqlem7  29548  2clwwlk2  29591  ex-po  29678  pliguhgr  29727  nvnd  29929  ipval2lem3  29946  ipval2  29948  ipidsq  29951  dipcj  29955  dip0r  29958  nmlnogt0  30038  blocni  30046  ipasslem2  30073  ipasslem8  30078  ipasslem9  30079  ajval  30102  ubthlem1  30111  hvaddlid  30264  hvsub0  30317  hi02  30338  hlimi  30429  isch2  30464  chlimi  30475  chsupunss  30585  shsupunss  30587  chlejb1i  30717  h1dei  30791  h1de2ci  30797  spanunsni  30820  pjoml2i  30826  pjorthi  30910  mayete3i  30969  hosubid1  31039  nmopge0  31152  nmfnge0  31168  adj1  31174  adjeq  31176  lnop0  31207  lnopmi  31241  nmophmi  31272  cnlnadjlem5  31312  cnlnadjeui  31318  unierri  31345  leoprf2  31368  leopnmid  31379  nmopleid  31380  hstles  31472  hst0  31474  strlem3a  31493  dmdbr2  31544  mdsl1i  31562  mdsl2i  31563  mdsl2bi  31564  cvmdi  31565  mdslmd1lem1  31566  mdslmd1lem2  31567  mdslmd1i  31570  mdslmd2i  31571  csmdsymi  31575  mdexchi  31576  superpos  31595  atomli  31623  atordi  31625  chirredlem1  31631  chirredlem2  31632  atcvat4i  31638  atabsi  31642  mdsymlem1  31644  mdsymlem5  31648  mdsymlem6  31649  sumdmdii  31656  dmdbr5ati  31663  dmdbr6ati  31664  mddmdin0i  31672  cdj3lem2  31676  unidifsnel  31760  unidifsnne  31761  xppreima  31859  abfmpunirn  31865  abfmpel  31868  aciunf1lem  31875  fgreu  31885  imafi2  31924  padct  31932  fpwrelmapffslem  31945  fpwrelmap  31946  xrge0infss  31961  xrdifh  31979  pfx1s2  32093  clatp0cl  32134  clatp1cl  32135  cntrcrng  32202  cycpmco2lem4  32276  rmfsupp2  32376  1fldgenq  32401  resvval  32430  rearchi  32450  qusxpid  32464  fermltlchr  32467  opprabs  32585  rlmdim  32683  locfinreflem  32809  locfinref  32810  ordtconnlem1  32893  rge0scvg  32918  lmxrge0  32921  qqh0  32953  qqh1  32954  rrh0  32984  zrhre  32988  esumcst  33050  esumfzf  33056  esumfsupre  33058  hasheuni  33072  sgon  33111  dmvlsiga  33116  sigainb  33123  measval  33185  ismeas  33186  sxbrsigalem0  33259  omssubadd  33288  carsggect  33306  eulerpartlemmf  33363  eulerpartlemgs2  33368  eulerpartlemn  33369  rrvsum  33442  ballotlem2  33476  ballotlemfcc  33481  ballotlem4  33486  signsplypnf  33550  signsply0  33551  signsw0glem  33553  signswrid  33558  signlem0  33587  signshf  33588  bnj535  33890  bnj580  33913  bnj907  33967  bnj1253  34017  funen1cnv  34080  loop1cycl  34117  ptpconn  34213  cvmsss2  34254  cvmlift2lem12  34294  cvmlift2lem13  34295  cvmliftphtlem  34297  cvmliftpht  34298  fmlafvel  34365  mppsthm  34559  bcneg1  34695  fv1stcnv  34737  fv2ndcnv  34738  wlimeq1  34781  imagesset  34914  altopeq1  34924  brcolinear2  35019  gg-negcncf  35155  cldbnd  35200  ivthALT  35209  refssfne  35232  ontgval  35305  onint1  35323  axc11n11r  35550  bj-pm11.53a  35645  bj-bm1.3ii  35934  bj-restsn0  35955  bj-restsn10  35956  bj-restsnid  35957  bj-rest10  35958  bj-rest0  35963  bj-inftyexpiinv  36078  bj-inftyexpidisj  36080  taupilem1  36191  irrdiff  36196  f1omptsnlem  36206  mptsnunlem  36208  topdifinffinlem  36217  inunissunidif  36245  rdgssun  36248  exrecfnlem  36249  exrecfnpw  36251  finixpnum  36462  tan2h  36469  matunitlindflem2  36474  ptrest  36476  poimirlem22  36499  poimirlem25  36502  mblfinlem1  36514  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2addnclem  36528  itg2addnclem2  36529  itg2addnclem3  36530  itg2addnc  36531  itg2gt0cn  36532  ftc1anclem5  36554  ftc1anclem8  36557  dvasin  36561  dvacos  36562  sdclem2  36599  totbndbnd  36646  heibor1lem  36666  heiborlem7  36674  bfplem1  36679  prnc  36924  ecexALTV  37189  brxrn  37233  riotasv  37818  glbconN  38236  glbconNOLD  38237  atpointN  38603  polsubN  38767  pol0N  38769  pol1N  38770  2polvalN  38774  2polssN  38775  3polN  38776  pcl0N  38782  2pmaplubN  38786  pnonsingN  38793  polsubclN  38812  cdlemefs32sn1aw  39274  cdleme43fsv1snlem  39280  cdleme41sn3a  39293  cdleme32a  39301  cdleme40m  39327  cdleme40n  39328  cdleme42b  39338  istendo  39620  cdlemk40  39777  cdlemkid  39796  dihvalcqpre  40095  facp2  40948  fac2xp3  41009  2xp3dxp2ge1d  41011  factwoffsmonot  41012  fnsnbt  41049  frlmsnic  41108  relt0neg1  41314  sn-nnne0  41318  sn-inelr  41335  prjspnerlem  41356  prjspnval2  41357  0prjspn  41367  3cubes  41414  mapfzcons1cl  41442  eldioph3b  41489  eldiophss  41498  0dioph  41502  vdioph  41503  eldioph4b  41535  eldioph4i  41536  rencldnfilem  41544  rmxy1  41647  rmxy0  41648  rmxm1  41659  rmym1  41660  monotoddzzfi  41667  wepwso  41771  aomclem6  41787  pwslnmlem0  41819  isnumbasabl  41834  areaquad  41951  onexlimgt  41978  oaabsb  42030  nadd1suc  42128  om2  42141  oe2  42143  safesnsupfidom1o  42154  onno  42170  oa1cl  42184  finona1cl  42190  reabsifneg  42369  reabsifnneg  42372  relexp2  42414  eltrclrec  42417  elrtrclrec  42418  brtrclrec  42433  brrtrclrec  42434  relexpxpmin  42454  dftrcl3  42457  dfrtrcl3  42470  heeq1  42514  seff  43054  lhe4.4ex1a  43074  eelT0  43522  snssl  43577  sineq0ALT  43684  elabrexg  43714  elrnmpt1sf  43873  founiiun0  43874  supxrgere  44030  supxrgelem  44034  fmuldfeqlem1  44285  fmuldfeq  44286  climneg  44313  sumnnodd  44333  liminfltlem  44507  xlimpnfxnegmnf2  44561  addccncf2  44579  dvsinax  44616  stoweidlem18  44721  stoweidlem19  44722  stoweidlem22  44725  stoweidlem34  44737  stoweidlem40  44743  stoweidlem41  44744  stoweidlem55  44758  stoweidlem59  44762  dirker2re  44795  dirkerdenne0  44796  fourierdlem48  44857  fourierdlem49  44858  fourierdlem70  44879  fourierdlem71  44880  fourierdlem104  44913  fourierdlem112  44921  fouriersw  44934  etransclem46  44983  etransclem48  44985  nnfoctbdjlem  45158  natlocalincr  45577  singoutnword  45583  upwrdfi  45588  sqrtnegnre  46002  fsummmodsnunz  46030  flsqrt5  46249  bits0ALTV  46334  mogoldbblem  46375  sgoldbeven3prm  46438  nnsum3primes4  46443  ushrisomgr  46496  subrngint  46724  2zrngnmlid  46801  2zrngnmrid  46802  mpoexxg2  46967  lco0  47062  zlmodzxzldeplem3  47137  0dig1  47249  naryfvalel  47270  ackvalsuc0val  47327  aacllem  47802