Theorem mp2an 430

Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)

Hypotheses

Ref	Expression
mp2an.1	⊢ 𝜑
mp2an.2	⊢ 𝜓
mp2an.3	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mp2an	⊢ 𝜒

Proof of Theorem mp2an

Step	Hyp	Ref	Expression
1		mp2an.2	. 2 ⊢ 𝜓
2		mp2an.1	. . 3 ⊢ 𝜑
3		mp2an.3	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	2, 3	mpan 428	. 2 ⊢ (𝜓 → 𝜒)
5	1, 4	ax-mp 5	1 ⊢ 𝜒

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mp4an  431  jaoi  728  mp3an  1378  barbara  2185  eqeq12i  2252  el2v  2827  vtocl2  2878  spc2ev  2921  sbc2ie  3123  csbieb  3189  sseq12i  3276  uneq12i  3381  ineq12i  3430  ifssun  3655  nelpri  3733  ralpr  3764  rexpr  3765  preq12i  3793  dfop  3903  opeq12i  3909  breq12i  4140  mpteq2ia  4219  exmidundif  4345  exmidundifim  4346  opex  4371  opi2  4375  opth2  4382  opeqsn  4395  opeqpr  4396  uniop  4398  opelopaba  4410  braba  4411  opelopab  4416  brab  4417  opelopabaf  4418  unex  4589  snnex  4596  op1stb  4626  ifelpwun  4631  ifex  4634  onun2i  4640  onsucssi  4655  ontriexmidim  4671  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  opthreg  4705  tfis  4732  finds  4749  finds2  4750  nnregexmid  4770  xpeq12i  4798  opelvv  4827  eqrelriiv  4871  eqrelrdv  4873  xpss  4885  xpex  4893  relop  4932  brco  4953  opelcnv  4964  brcnv  4965  asymref  5176  codir  5179  ssrnres  5233  dmprop  5265  dfco2  5290  cossxp  5313  cocnvss  5316  coex  5336  funsn  5432  fnsn  5438  feq23i  5531  resasplitss  5572  fabex  5583  fvex  5718  xpsn  5888  fmptap  5908  opabex  5944  rinvf1o  6038  acexmidlemv  6086  oveq12i  6100  oprabid  6120  oprabss  6177  caovcom  6250  opabex3  6355  iunex  6356  oprabex  6365  ofmres  6373  op1st  6384  op2nd  6385  fo1st  6395  fo2nd  6396  mpoex  6454  1stconst  6461  2ndconst  6462  algrflem  6469  dftpos4  6539  tpostpos  6540  tpossym  6552  frecex  6670  frecfnom  6677  2oex  6709  sucinc  6723  fnoei  6730  oeiexg  6731  nnacli  6760  nnmcli  6761  elec  6853  ecovcom  6921  ecovass  6923  ecovdi  6925  fnmap  6934  mapval  6939  elmap  6963  elpm  6965  elpm2  6966  map0  6977  ixpconst  6996  entri  7079  endisj  7128  xpcomco  7130  phplem2  7160  1ndom2  7172  ssfiexmid  7184  domfiexmid  7188  exmidpw2en  7225  unfiexmid  7231  unfiin  7239  inresflem  7407  casefun  7432  caserel  7434  caseinj  7436  omp1eomlem  7441  omp1eom  7442  endjusym  7443  djufun  7451  djuinj  7453  ctssdccl  7458  ctssdclemr  7459  nninfex  7468  infnninf  7471  fodjuomnilemdc  7491  ctssexmid  7497  exmidonfinlem  7552  dju1p1e2  7556  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  exmidaclem  7571  pw1dom2  7593  onntri35  7603  onntri45  7607  2oneel  7629  2omotaplemst  7631  acnccim  7645  1lt2pi  7714  indpi  7716  1nq  7740  rec1nq  7769  1lt2nq  7780  ltaddnq  7781  halfnqq  7784  prarloclemarch2  7793  prarloclemlt  7867  prarloclemcalc  7876  genpelxp  7885  ltexprlempr  7982  recexprlempr  8006  cauappcvgprlemcl  8027  cauappcvgprlemladd  8032  caucvgprlemcl  8050  caucvgprprlemcl  8078  suplocexprlemell  8087  suplocexprlemdisj  8094  suplocexprlemub  8097  0r  8124  1sr  8125  m1r  8126  m1p1sr  8134  m1m1sr  8135  0lt1sr  8139  1ne0sr  8140  1idsr  8142  recexgt0sr  8147  prsradd  8160  caucvgsrlemoffres  8174  caucvgsr  8176  mappsrprg  8178  map2psrprg  8179  pitonnlem1p1  8220  pitonnlem2  8221  pitoregt0  8223  peano2nnnn  8227  axi2m1  8249  axprecex  8254  axcnre  8255  nnindnn  8267  nntopi  8268  0cn  8325  addcli  8337  mulcli  8338  mulcomi  8339  readdcli  8346  remulcli  8347  rexpssxrxp  8377  ltrelxr  8393  gtneii  8429  lttri3i  8431  letri3i  8432  ltnsymi  8433  lenlti  8434  ltlei  8435  mulgt0i  8443  mulgt0ii  8444  0lt1  8461  addcomi  8478  pncan3oi  8550  resubcli  8597  subcli  8610  pncan3i  8611  negsubi  8612  subnegi  8613  subeq0i  8614  neg11i  8615  negcon1i  8616  negcon2i  8617  mulneg1i  8739  mulneg2i  8740  mul2negi  8741  addgt0ii  8827  ltnegi  8829  lenegi  8830  ltnegcon2i  8831  lesub0i  8832  ltaddposi  8833  posdifi  8834  ltnegcon1i  8835  lenegcon1i  8836  subge0i  8837  1ap0  8927  ltapii  8972  recrecapi  9083  dividapi  9084  div0api  9085  rec11apii  9100  divdiv32api  9106  recgt0ii  9246  ltrecii  9257  ltdiv23ii  9266  sup3exmid  9296  nnssre  9318  nnind  9330  nnmulcli  9336  nnsubi  9354  0le2  9404  1lt3  9488  2lt4  9490  1lt4  9491  3lt5  9493  2lt5  9494  1lt5  9495  4lt6  9497  3lt6  9498  2lt6  9499  1lt6  9500  5lt7  9502  4lt7  9503  3lt7  9504  2lt7  9505  1lt7  9506  6lt8  9508  5lt8  9509  4lt8  9510  3lt8  9511  2lt8  9512  1lt8  9513  7lt9  9515  6lt9  9516  5lt9  9517  4lt9  9518  3lt9  9519  2lt9  9520  1lt9  9521  2muline0  9542  nn0addcli  9612  nn0mulcli  9613  nn0addge1i  9623  nn0addge2i  9624  dfz2  9727  halfnz  9753  9p1e10  9790  numnncl  9797  numltc  9818  le9lt10  9819  nummac  9837  8lt10  9924  7lt10  9925  6lt10  9926  5lt10  9927  4lt10  9928  3lt10  9929  2lt10  9930  1lt10  9931  eluzaddi  9965  eluzsubi  9966  uzuzle23  9978  uzuzle24  9979  uzuzle34  9980  eluz2nn  9982  eluz4eluz2  9984  eluzge3nn  9988  divfnzn  10037  elq  10038  qreccl  10058  xrltnr  10198  mnfltpnf  10204  xaddmnf1  10267  pnfaddmnf  10269  mnfaddpnf  10270  xrex  10275  xaddid1  10281  xsubge0  10300  xposdif  10301  xleaddadd  10306  elicc2i  10358  ioomax  10367  iccmax  10368  ioopos  10369  elxrge0  10397  iccshftri  10414  iccshftli  10416  iccdili  10418  icccntri  10420  unitssre  10425  fz10  10467  fz00m1  10468  fzpreddisj  10495  fz0to4untppr  10548  dfrp2  10715  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  frecfzennn  10884  xnn0nnen  10895  fnn0nninf  10896  fxnn0nninf  10897  0tonninf  10898  1tonninf  10899  m1expcl2  11019  m1expcl  11020  nn0expcli  11023  sqmuli  11080  cu2  11096  i3  11099  subsqi  11107  binom2subi  11113  bcpasc  11226  4bc2eq6  11235  hashinfom  11239  prhash2ex  11272  hashp1i  11273  lsw0g  11375  swrdccat3blem  11533  rei  11687  imi  11688  readdi  11716  imaddi  11717  remuli  11718  immuli  11719  cjaddi  11720  cjmuli  11721  ipcni  11722  crrei  11724  crimi  11725  rexfiuz  11777  sqrt1  11834  sqrt4  11835  sqrt9  11836  abs1  11860  sqrtmulii  11923  abslti  11927  abslei  11928  abssubi  11939  absmuli  11940  sqabsaddi  11941  sqabssubi  11942  abstrii  11944  fimaxre2  12016  fiidxsupcl  12018  climz  12083  abscn2  12106  recn2  12108  imcn2  12109  climabs  12111  climre  12113  climim  12114  fsumcnv  12229  fsumrelem  12263  fsumre  12264  fsumim  12265  arisum2  12291  expcnv  12296  geo2sum2  12307  geo2lim  12308  0.999...  12313  geoihalfsum  12314  fprodcnv  12417  fprodge0  12429  fprodge1  12431  ege2le3  12463  ef0  12464  reeff1  12492  tan0  12523  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  sinltxirr  12553  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  sincos1sgn  12557  sincos2sgn  12558  cos12dec  12560  egt2lt3  12572  epos  12573  ene1  12577  eap1  12578  3dvds  12656  3dvdsdec  12657  3dvds2dec  12658  odd2np1lem  12664  n2dvds1  12704  z4even  12708  ndvdsi  12725  flodddiv4  12728  bitsp1o  12745  0bits  12751  gcd0val  12762  6gcd4e2  12797  3lcm2e6woprm  12889  6lcm4e12  12890  3lcm2e6  12964  sqrt2irrlem  12965  phimullem  13032  pockthi  13166  4sqlem19  13217  dec2dvds  13219  dec5dvds2  13221  dec2nprm  13223  modxai  13224  mod2xnegi  13227  gcdi  13229  gcdmodi  13230  numexpp1  13233  karatsuba  13239  2exp7  13243  1259lem4  13274  1259lem5  13275  1259prm  13276  ballotfilemofi  13277  ballotfilem1  13278  ballotfilem2  13286  ballotfilemfmpn  13292  ballotfilemefi  13295  ballotfilemodife  13298  ballotfilem4  13299  ballotfilemiex  13302  ballotfilemimin  13307  ballotfilemic  13308  ballotfilemsval  13310  ballotfilemsdom  13313  ballotfilemsel1i  13314  ballotfilemsima  13317  ballotfilemrval  13319  ballotfilemfrceq  13330  ballotfilemfrcn0  13331  ballotfilem1ri  13336  ballotfilem7  13337  ballotfilem8  13338  ballotfilemth  13339  xpnnen  13343  xpomen  13344  ennnfonelemj0  13350  ennnfonelem0  13354  ennnfonelemhf1o  13362  exmidunben  13375  qnnen  13380  unct  13391  setscom  13450  strleun  13517  prdsvallem  13680  imasival  13686  ismgm  13736  fn0g  13754  fngzsum  13767  issgrp  13777  ismnddef  13790  isghm  14105  prdsex  14279  isrng  14340  rngmgpf  14343  isring  14411  mgpf  14422  dfrhm2  14570  rhmex  14573  isdomn  14687  rmodislmod  14797  lidlmex  14921  mopnset  14998  cnfldstr  15004  cnfldcj  15011  cnfld0  15017  cnfldplusf  15020  zringcrng  15036  zringmulr  15043  zringmpg  15050  znval  15080  psrval  15161  fnpsr  15162  psrbagmaxlem1  15185  fnmpl  15237  txtopi  15520  txunii  15523  upxp  15531  uptx  15533  cnmpt1st  15547  cnmpt2nd  15548  txswaphmeolem  15579  qtopbasss  15780  cnmet  15789  cnfldms  15795  cnopncntop  15803  cnopn  15804  remet  15807  blssioo  15812  tgqioo  15814  tgioo2cntop  15816  tgioo2  15818  divcnap  15824  abscncf  15844  recncf  15845  imcncf  15846  cjcncf  15847  mulc1cncf  15848  cncfcn1cntop  15853  idcncf  15860  cdivcncfap  15863  expcncf  15868  cnrehmeocntop  15869  maxcncf  15874  mincncf  15875  ivthreinc  15904  hovercncf  15905  limccnp2lem  15935  limccnp2cntop  15936  dvcnp2cntop  15958  dvaddxxbr  15960  dvmulxxbr  15961  dvcoapbr  15966  dvrecap  15972  dveflem  15985  dvef  15986  sincn  16028  coscn  16029  reeff1oleme  16031  reeff1o  16032  cosz12  16040  sin0pilem1  16041  sin0pilem2  16042  pipos  16048  sinhalfpilem  16051  sincosq1lem  16085  sincosq1sgn  16086  sincosq2sgn  16087  sincosq3sgn  16088  sincosq4sgn  16089  sinq12gt0  16090  cosq14gt0  16092  cosq23lt0  16093  coseq0q4123  16094  coseq00topi  16095  coseq0negpitopi  16096  tangtx  16098  sincos4thpi  16100  tan4thpi  16101  sincos6thpi  16102  pigt3  16104  cosordlem  16110  cosq34lt1  16111  cos02pilt1  16112  cos0pilt1  16113  ioocosf1o  16115  negpitopissre  16116  log1  16128  loge  16129  2logb9irr  16240  sqrt2cxp2logb9e3  16244  2logb9irrap  16246  log2tlbndlog2  16253  log2ublem1  16254  log2ublem2  16255  log2ublem3  16256  log2ublog2  16257  birthdaylog2  16261  ppi1  16303  cht1  16304  ppi1i  16305  ppi2i  16306  cht2  16309  cht3  16310  chtqrpcl  16312  mpodvdsmulf1o  16317  fsumdvdsmul  16318  1sgm2ppw  16322  ppiublem1  16324  ppiublem2  16325  ppiqub  16326  chtqub  16329  bpos1lem  16342  bposlem6  16349  bposlem7  16350  bposlem8  16351  bposlem9  16352  lgsdir2lem2  16386  lgsdir2lem3  16387  lgseisenlem4  16430  2lgsoddprmlem3  16468  2sqlem9  16481  2sqlem10  16482  opvtxfvi  16506  opiedgfvi  16507  umgrbien  16589  usgrprc  16731  vtxdfifiun  16776  upgr2wlkdc  16856  konigsbergvtx  16961  konigsbergiedg  16962  konigsbergumgr  16966  konigsberglem1  16967  konigsberglem2  16968  konigsberglem3  16969  konigsberglem5  16971  konigsberg  16972  ex-fl  16977  ex-ceil  16978  ex-bc  16981  ex-dvds  16982  ex-gcd  16983  bj-charfunbi  17075  bj-unex  17183  bj-nn0suc0  17214  bj-nntrans  17215  bj-nnelirr  17217  012of  17261  2o01f  17262  pwle2  17266  nnsf  17287  peano3nninf  17289  exmidsbthrlem  17306  sbthom  17310  repiecelem  17313  repiecele0  17314  repiecege0  17315  isomninnlem  17318  iooref1o  17322  trilpolemisumle  17327  trilpolemeq1  17329  trilpolemlt1  17330  apdiff  17337  iswomninnlem  17339  iswomni0  17341  ismkvnnlem  17342  dceqnconst  17350  dcapnconst  17351  nconstwlpolemgt0  17354  taupi  17363