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  4139  mpteq2ia  4217  exmidundif  4343  exmidundifim  4344  opex  4369  opi2  4373  opth2  4380  opeqsn  4393  opeqpr  4394  uniop  4396  opelopaba  4408  braba  4409  opelopab  4414  brab  4415  opelopabaf  4416  unex  4587  snnex  4594  op1stb  4624  ifelpwun  4629  ifex  4632  onun2i  4638  onsucssi  4653  ontriexmidim  4669  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  opthreg  4703  tfis  4730  finds  4747  finds2  4748  nnregexmid  4768  xpeq12i  4796  opelvv  4825  eqrelriiv  4869  eqrelrdv  4871  xpss  4883  xpex  4891  relop  4930  brco  4951  opelcnv  4962  brcnv  4963  asymref  5173  codir  5176  ssrnres  5230  dmprop  5262  dfco2  5287  cossxp  5310  cocnvss  5313  coex  5333  funsn  5429  fnsn  5435  feq23i  5528  resasplitss  5569  fabex  5580  fvex  5715  xpsn  5885  fmptap  5905  opabex  5941  rinvf1o  6035  acexmidlemv  6083  oveq12i  6097  oprabid  6117  oprabss  6174  caovcom  6247  opabex3  6351  iunex  6352  oprabex  6361  ofmres  6369  op1st  6380  op2nd  6381  fo1st  6391  fo2nd  6392  mpoex  6450  1stconst  6457  2ndconst  6458  algrflem  6465  dftpos4  6534  tpostpos  6535  tpossym  6547  frecex  6665  frecfnom  6672  2oex  6704  sucinc  6718  fnoei  6725  oeiexg  6726  nnacli  6755  nnmcli  6756  elec  6848  ecovcom  6916  ecovass  6918  ecovdi  6920  fnmap  6929  mapval  6934  elmap  6958  elpm  6960  elpm2  6961  map0  6971  ixpconst  6990  entri  7073  endisj  7122  xpcomco  7124  phplem2  7154  1ndom2  7166  ssfiexmid  7178  domfiexmid  7182  exmidpw2en  7219  unfiexmid  7225  unfiin  7233  inresflem  7400  casefun  7425  caserel  7427  caseinj  7429  omp1eomlem  7434  omp1eom  7435  endjusym  7436  djufun  7444  djuinj  7446  ctssdccl  7451  ctssdclemr  7452  nninfex  7461  infnninf  7464  fodjuomnilemdc  7484  ctssexmid  7490  exmidonfinlem  7545  dju1p1e2  7549  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  pw1dom2  7586  onntri35  7596  onntri45  7600  2oneel  7622  2omotaplemst  7624  acnccim  7638  1lt2pi  7707  indpi  7709  1nq  7733  rec1nq  7762  1lt2nq  7773  ltaddnq  7774  halfnqq  7777  prarloclemarch2  7786  prarloclemlt  7860  prarloclemcalc  7869  genpelxp  7878  ltexprlempr  7975  recexprlempr  7999  cauappcvgprlemcl  8020  cauappcvgprlemladd  8025  caucvgprlemcl  8043  caucvgprprlemcl  8071  suplocexprlemell  8080  suplocexprlemdisj  8087  suplocexprlemub  8090  0r  8117  1sr  8118  m1r  8119  m1p1sr  8127  m1m1sr  8128  0lt1sr  8132  1ne0sr  8133  1idsr  8135  recexgt0sr  8140  prsradd  8153  caucvgsrlemoffres  8167  caucvgsr  8169  mappsrprg  8171  map2psrprg  8172  pitonnlem1p1  8213  pitonnlem2  8214  pitoregt0  8216  peano2nnnn  8220  axi2m1  8242  axprecex  8247  axcnre  8248  nnindnn  8260  nntopi  8261  0cn  8318  addcli  8330  mulcli  8331  mulcomi  8332  readdcli  8339  remulcli  8340  rexpssxrxp  8370  ltrelxr  8386  gtneii  8421  lttri3i  8423  letri3i  8424  ltnsymi  8425  lenlti  8426  ltlei  8427  mulgt0i  8435  mulgt0ii  8436  0lt1  8453  addcomi  8470  pncan3oi  8542  resubcli  8589  subcli  8602  pncan3i  8603  negsubi  8604  subnegi  8605  subeq0i  8606  neg11i  8607  negcon1i  8608  negcon2i  8609  mulneg1i  8731  mulneg2i  8732  mul2negi  8733  addgt0ii  8819  ltnegi  8821  lenegi  8822  ltnegcon2i  8823  lesub0i  8824  ltaddposi  8825  posdifi  8826  ltnegcon1i  8827  lenegcon1i  8828  subge0i  8829  1ap0  8919  ltapii  8964  recrecapi  9075  dividapi  9076  div0api  9077  rec11apii  9092  divdiv32api  9098  recgt0ii  9238  ltrecii  9249  ltdiv23ii  9258  sup3exmid  9288  nnssre  9309  nnind  9321  nnmulcli  9327  nnsubi  9345  0le2  9395  1lt3  9478  2lt4  9480  1lt4  9481  3lt5  9483  2lt5  9484  1lt5  9485  4lt6  9487  3lt6  9488  2lt6  9489  1lt6  9490  5lt7  9492  4lt7  9493  3lt7  9494  2lt7  9495  1lt7  9496  6lt8  9498  5lt8  9499  4lt8  9500  3lt8  9501  2lt8  9502  1lt8  9503  7lt9  9505  6lt9  9506  5lt9  9507  4lt9  9508  3lt9  9509  2lt9  9510  1lt9  9511  2muline0  9532  nn0addcli  9602  nn0mulcli  9603  nn0addge1i  9613  nn0addge2i  9614  dfz2  9719  halfnz  9744  9p1e10  9781  numnncl  9788  numltc  9804  le9lt10  9805  nummac  9823  8lt10  9910  7lt10  9911  6lt10  9912  5lt10  9913  4lt10  9914  3lt10  9915  2lt10  9916  1lt10  9917  eluzaddi  9951  eluzsubi  9952  uzuzle23  9964  uzuzle24  9965  uzuzle34  9966  eluz2nn  9968  eluz4eluz2  9970  eluzge3nn  9974  divfnzn  10023  elq  10024  qreccl  10044  xrltnr  10183  mnfltpnf  10189  xaddmnf1  10252  pnfaddmnf  10254  mnfaddpnf  10255  xrex  10260  xaddid1  10266  xsubge0  10285  xposdif  10286  xleaddadd  10291  elicc2i  10343  ioomax  10352  iccmax  10353  ioopos  10354  elxrge0  10382  iccshftri  10399  iccshftli  10401  iccdili  10403  icccntri  10405  unitssre  10410  fz10  10452  fz00m1  10453  fzpreddisj  10480  fz0to4untppr  10533  dfrp2  10700  fldiv4p1lem1div2  10742  fldiv4lem1div2  10744  frecfzennn  10865  xnn0nnen  10876  fnn0nninf  10877  fxnn0nninf  10878  0tonninf  10879  1tonninf  10880  m1expcl2  11000  m1expcl  11001  nn0expcli  11004  sqmuli  11061  cu2  11077  i3  11080  subsqi  11088  binom2subi  11094  bcpasc  11206  4bc2eq6  11215  hashinfom  11219  prhash2ex  11252  hashp1i  11253  lsw0g  11355  swrdccat3blem  11513  rei  11667  imi  11668  readdi  11696  imaddi  11697  remuli  11698  immuli  11699  cjaddi  11700  cjmuli  11701  ipcni  11702  crrei  11704  crimi  11705  rexfiuz  11757  sqrt1  11814  sqrt4  11815  sqrt9  11816  abs1  11840  sqrtmulii  11902  abslti  11906  abslei  11907  abssubi  11918  absmuli  11919  sqabsaddi  11920  sqabssubi  11921  abstrii  11923  fimaxre2  11995  climz  12060  abscn2  12083  recn2  12085  imcn2  12086  climabs  12088  climre  12090  climim  12091  fsumcnv  12206  fsumrelem  12240  fsumre  12241  fsumim  12242  arisum2  12268  expcnv  12273  geo2sum2  12284  geo2lim  12285  0.999...  12290  geoihalfsum  12291  fprodcnv  12394  fprodge0  12406  fprodge1  12408  ege2le3  12440  ef0  12441  reeff1  12469  tan0  12500  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  cos1bnd  12528  cos2bnd  12529  sinltxirr  12530  sin01gt0  12531  cos01gt0  12532  sin02gt0  12533  sincos1sgn  12534  sincos2sgn  12535  cos12dec  12537  egt2lt3  12549  epos  12550  ene1  12554  eap1  12555  3dvds  12633  3dvdsdec  12634  3dvds2dec  12635  odd2np1lem  12641  n2dvds1  12681  z4even  12685  ndvdsi  12702  flodddiv4  12705  bitsp1o  12722  0bits  12728  gcd0val  12739  6gcd4e2  12774  3lcm2e6woprm  12866  6lcm4e12  12867  3lcm2e6  12940  sqrt2irrlem  12941  phimullem  13005  pockthi  13139  4sqlem19  13190  dec2dvds  13192  dec5dvds2  13194  dec2nprm  13196  modxai  13197  gcdi  13201  gcdmodi  13202  numexpp1  13205  karatsuba  13211  2exp7  13215  ballotfilemofi  13221  ballotfilem1  13222  ballotfilem2  13230  ballotfilemfmpn  13236  ballotfilemefi  13239  ballotfilemodife  13242  ballotfilem4  13243  ballotfilemiex  13246  ballotfilemimin  13251  ballotfilemic  13252  ballotfilemsval  13254  ballotfilemsdom  13257  ballotfilemsel1i  13258  ballotfilemsima  13261  ballotfilemrval  13263  ballotfilemfrceq  13274  ballotfilemfrcn0  13275  ballotfilem1ri  13280  ballotfilem7  13281  ballotfilem8  13282  ballotfilemth  13283  xpnnen  13287  xpomen  13288  ennnfonelemj0  13294  ennnfonelem0  13298  ennnfonelemhf1o  13306  exmidunben  13319  qnnen  13324  unct  13335  setscom  13394  strleun  13460  prdsvallem  13623  imasival  13629  ismgm  13679  fn0g  13697  fngzsum  13710  issgrp  13720  ismnddef  13733  isghm  14048  prdsex  14174  isrng  14235  rngmgpf  14238  isring  14306  mgpf  14317  dfrhm2  14463  rhmex  14466  isdomn  14580  rmodislmod  14690  lidlmex  14814  mopnset  14891  cnfldstr  14897  cnfldcj  14904  cnfld0  14910  cnfldplusf  14913  zringcrng  14929  zringmulr  14936  zringmpg  14943  znval  14973  psrval  15052  fnpsr  15053  fnmpl  15086  txtopi  15364  txunii  15367  upxp  15375  uptx  15377  cnmpt1st  15391  cnmpt2nd  15392  txswaphmeolem  15423  qtopbasss  15624  cnmet  15633  cnfldms  15639  cnopncntop  15647  cnopn  15648  remet  15651  blssioo  15656  tgqioo  15658  tgioo2cntop  15660  tgioo2  15662  divcnap  15668  abscncf  15688  recncf  15689  imcncf  15690  cjcncf  15691  mulc1cncf  15692  cncfcn1cntop  15697  idcncf  15704  cdivcncfap  15707  expcncf  15712  cnrehmeocntop  15713  maxcncf  15718  mincncf  15719  ivthreinc  15748  hovercncf  15749  limccnp2lem  15779  limccnp2cntop  15780  dvcnp2cntop  15802  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvrecap  15816  dveflem  15829  dvef  15830  sincn  15872  coscn  15873  reeff1oleme  15875  reeff1o  15876  cosz12  15884  sin0pilem1  15885  sin0pilem2  15886  pipos  15892  sinhalfpilem  15895  sincosq1lem  15929  sincosq1sgn  15930  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  sinq12gt0  15934  cosq14gt0  15936  cosq23lt0  15937  coseq0q4123  15938  coseq00topi  15939  coseq0negpitopi  15940  tangtx  15942  sincos4thpi  15944  tan4thpi  15945  sincos6thpi  15946  pigt3  15948  cosordlem  15953  cosq34lt1  15954  cos02pilt1  15955  cos0pilt1  15956  ioocosf1o  15958  negpitopissre  15959  log1  15970  loge  15971  2logb9irr  16079  sqrt2cxp2logb9e3  16083  2logb9irrap  16085  log2tlbndlog2  16088  log2ublem1  16089  log2ublem2  16090  log2ublem3  16091  log2ublog2  16092  birthdaylog2  16096  mpodvdsmulf1o  16110  fsumdvdsmul  16111  1sgm2ppw  16115  lgsdir2lem2  16160  lgsdir2lem3  16161  lgseisenlem4  16204  2lgsoddprmlem3  16242  2sqlem9  16255  2sqlem10  16256  opvtxfvi  16280  opiedgfvi  16281  umgrbien  16363  usgrprc  16505  vtxdfifiun  16550  upgr2wlkdc  16630  konigsbergvtx  16735  konigsbergiedg  16736  konigsbergumgr  16740  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  konigsberglem5  16745  konigsberg  16746  ex-fl  16751  ex-ceil  16752  ex-bc  16755  ex-dvds  16756  ex-gcd  16757  bj-charfunbi  16849  bj-unex  16957  bj-nn0suc0  16988  bj-nntrans  16989  bj-nnelirr  16991  012of  17035  2o01f  17036  pwle2  17040  nnsf  17060  peano3nninf  17062  exmidsbthrlem  17079  sbthom  17083  repiecelem  17086  repiecele0  17087  repiecege0  17088  isomninnlem  17091  iooref1o  17095  trilpolemisumle  17099  trilpolemeq1  17101  trilpolemlt1  17102  apdiff  17109  iswomninnlem  17111  iswomni0  17113  ismkvnnlem  17114  dceqnconst  17122  dcapnconst  17123  nconstwlpolemgt0  17126  taupi  17135