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  7401  casefun  7426  caserel  7428  caseinj  7430  omp1eomlem  7435  omp1eom  7436  endjusym  7437  djufun  7445  djuinj  7447  ctssdccl  7452  ctssdclemr  7453  nninfex  7462  infnninf  7465  fodjuomnilemdc  7485  ctssexmid  7491  exmidonfinlem  7546  dju1p1e2  7550  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  pw1dom2  7587  onntri35  7597  onntri45  7601  2oneel  7623  2omotaplemst  7625  acnccim  7639  1lt2pi  7708  indpi  7710  1nq  7734  rec1nq  7763  1lt2nq  7774  ltaddnq  7775  halfnqq  7778  prarloclemarch2  7787  prarloclemlt  7861  prarloclemcalc  7870  genpelxp  7879  ltexprlempr  7976  recexprlempr  8000  cauappcvgprlemcl  8021  cauappcvgprlemladd  8026  caucvgprlemcl  8044  caucvgprprlemcl  8072  suplocexprlemell  8081  suplocexprlemdisj  8088  suplocexprlemub  8091  0r  8118  1sr  8119  m1r  8120  m1p1sr  8128  m1m1sr  8129  0lt1sr  8133  1ne0sr  8134  1idsr  8136  recexgt0sr  8141  prsradd  8154  caucvgsrlemoffres  8168  caucvgsr  8170  mappsrprg  8172  map2psrprg  8173  pitonnlem1p1  8214  pitonnlem2  8215  pitoregt0  8217  peano2nnnn  8221  axi2m1  8243  axprecex  8248  axcnre  8249  nnindnn  8261  nntopi  8262  0cn  8319  addcli  8331  mulcli  8332  mulcomi  8333  readdcli  8340  remulcli  8341  rexpssxrxp  8371  ltrelxr  8387  gtneii  8423  lttri3i  8425  letri3i  8426  ltnsymi  8427  lenlti  8428  ltlei  8429  mulgt0i  8437  mulgt0ii  8438  0lt1  8455  addcomi  8472  pncan3oi  8544  resubcli  8591  subcli  8604  pncan3i  8605  negsubi  8606  subnegi  8607  subeq0i  8608  neg11i  8609  negcon1i  8610  negcon2i  8611  mulneg1i  8733  mulneg2i  8734  mul2negi  8735  addgt0ii  8821  ltnegi  8823  lenegi  8824  ltnegcon2i  8825  lesub0i  8826  ltaddposi  8827  posdifi  8828  ltnegcon1i  8829  lenegcon1i  8830  subge0i  8831  1ap0  8921  ltapii  8966  recrecapi  9077  dividapi  9078  div0api  9079  rec11apii  9094  divdiv32api  9100  recgt0ii  9240  ltrecii  9251  ltdiv23ii  9260  sup3exmid  9290  nnssre  9311  nnind  9323  nnmulcli  9329  nnsubi  9347  0le2  9397  1lt3  9481  2lt4  9483  1lt4  9484  3lt5  9486  2lt5  9487  1lt5  9488  4lt6  9490  3lt6  9491  2lt6  9492  1lt6  9493  5lt7  9495  4lt7  9496  3lt7  9497  2lt7  9498  1lt7  9499  6lt8  9501  5lt8  9502  4lt8  9503  3lt8  9504  2lt8  9505  1lt8  9506  7lt9  9508  6lt9  9509  5lt9  9510  4lt9  9511  3lt9  9512  2lt9  9513  1lt9  9514  2muline0  9535  nn0addcli  9605  nn0mulcli  9606  nn0addge1i  9616  nn0addge2i  9617  dfz2  9722  halfnz  9747  9p1e10  9784  numnncl  9791  numltc  9812  le9lt10  9813  nummac  9831  8lt10  9918  7lt10  9919  6lt10  9920  5lt10  9921  4lt10  9922  3lt10  9923  2lt10  9924  1lt10  9925  eluzaddi  9959  eluzsubi  9960  uzuzle23  9972  uzuzle24  9973  uzuzle34  9974  eluz2nn  9976  eluz4eluz2  9978  eluzge3nn  9982  divfnzn  10031  elq  10032  qreccl  10052  xrltnr  10192  mnfltpnf  10198  xaddmnf1  10261  pnfaddmnf  10263  mnfaddpnf  10264  xrex  10269  xaddid1  10275  xsubge0  10294  xposdif  10295  xleaddadd  10300  elicc2i  10352  ioomax  10361  iccmax  10362  ioopos  10363  elxrge0  10391  iccshftri  10408  iccshftli  10410  iccdili  10412  icccntri  10414  unitssre  10419  fz10  10461  fz00m1  10462  fzpreddisj  10489  fz0to4untppr  10542  dfrp2  10709  fldiv4p1lem1div2  10754  fldiv4lem1div2  10756  frecfzennn  10877  xnn0nnen  10888  fnn0nninf  10889  fxnn0nninf  10890  0tonninf  10891  1tonninf  10892  m1expcl2  11012  m1expcl  11013  nn0expcli  11016  sqmuli  11073  cu2  11089  i3  11092  subsqi  11100  binom2subi  11106  bcpasc  11219  4bc2eq6  11228  hashinfom  11232  prhash2ex  11265  hashp1i  11266  lsw0g  11368  swrdccat3blem  11526  rei  11680  imi  11681  readdi  11709  imaddi  11710  remuli  11711  immuli  11712  cjaddi  11713  cjmuli  11714  ipcni  11715  crrei  11717  crimi  11718  rexfiuz  11770  sqrt1  11827  sqrt4  11828  sqrt9  11829  abs1  11853  sqrtmulii  11916  abslti  11920  abslei  11921  abssubi  11932  absmuli  11933  sqabsaddi  11934  sqabssubi  11935  abstrii  11937  fimaxre2  12009  fiidxsupcl  12011  climz  12076  abscn2  12099  recn2  12101  imcn2  12102  climabs  12104  climre  12106  climim  12107  fsumcnv  12222  fsumrelem  12256  fsumre  12257  fsumim  12258  arisum2  12284  expcnv  12289  geo2sum2  12300  geo2lim  12301  0.999...  12306  geoihalfsum  12307  fprodcnv  12410  fprodge0  12422  fprodge1  12424  ege2le3  12456  ef0  12457  reeff1  12485  tan0  12516  ef01bndlem  12541  sin01bnd  12542  cos01bnd  12543  cos1bnd  12544  cos2bnd  12545  sinltxirr  12546  sin01gt0  12547  cos01gt0  12548  sin02gt0  12549  sincos1sgn  12550  sincos2sgn  12551  cos12dec  12553  egt2lt3  12565  epos  12566  ene1  12570  eap1  12571  3dvds  12649  3dvdsdec  12650  3dvds2dec  12651  odd2np1lem  12657  n2dvds1  12697  z4even  12701  ndvdsi  12718  flodddiv4  12721  bitsp1o  12738  0bits  12744  gcd0val  12755  6gcd4e2  12790  3lcm2e6woprm  12882  6lcm4e12  12883  3lcm2e6  12957  sqrt2irrlem  12958  phimullem  13025  pockthi  13159  4sqlem19  13210  dec2dvds  13212  dec5dvds2  13214  dec2nprm  13216  modxai  13217  mod2xnegi  13220  gcdi  13222  gcdmodi  13223  numexpp1  13226  karatsuba  13232  2exp7  13236  1259lem4  13267  1259lem5  13268  1259prm  13269  ballotfilemofi  13270  ballotfilem1  13271  ballotfilem2  13279  ballotfilemfmpn  13285  ballotfilemefi  13288  ballotfilemodife  13291  ballotfilem4  13292  ballotfilemiex  13295  ballotfilemimin  13300  ballotfilemic  13301  ballotfilemsval  13303  ballotfilemsdom  13306  ballotfilemsel1i  13307  ballotfilemsima  13310  ballotfilemrval  13312  ballotfilemfrceq  13323  ballotfilemfrcn0  13324  ballotfilem1ri  13329  ballotfilem7  13330  ballotfilem8  13331  ballotfilemth  13332  xpnnen  13336  xpomen  13337  ennnfonelemj0  13343  ennnfonelem0  13347  ennnfonelemhf1o  13355  exmidunben  13368  qnnen  13373  unct  13384  setscom  13443  strleun  13509  prdsvallem  13672  imasival  13678  ismgm  13728  fn0g  13746  fngzsum  13759  issgrp  13769  ismnddef  13782  isghm  14097  prdsex  14223  isrng  14284  rngmgpf  14287  isring  14355  mgpf  14366  dfrhm2  14512  rhmex  14515  isdomn  14629  rmodislmod  14739  lidlmex  14863  mopnset  14940  cnfldstr  14946  cnfldcj  14953  cnfld0  14959  cnfldplusf  14962  zringcrng  14978  zringmulr  14985  zringmpg  14992  znval  15022  psrval  15101  fnpsr  15102  fnmpl  15136  txtopi  15414  txunii  15417  upxp  15425  uptx  15427  cnmpt1st  15441  cnmpt2nd  15442  txswaphmeolem  15473  qtopbasss  15674  cnmet  15683  cnfldms  15689  cnopncntop  15697  cnopn  15698  remet  15701  blssioo  15706  tgqioo  15708  tgioo2cntop  15710  tgioo2  15712  divcnap  15718  abscncf  15738  recncf  15739  imcncf  15740  cjcncf  15741  mulc1cncf  15742  cncfcn1cntop  15747  idcncf  15754  cdivcncfap  15757  expcncf  15762  cnrehmeocntop  15763  maxcncf  15768  mincncf  15769  ivthreinc  15798  hovercncf  15799  limccnp2lem  15829  limccnp2cntop  15830  dvcnp2cntop  15852  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  dvrecap  15866  dveflem  15879  dvef  15880  sincn  15922  coscn  15923  reeff1oleme  15925  reeff1o  15926  cosz12  15934  sin0pilem1  15935  sin0pilem2  15936  pipos  15942  sinhalfpilem  15945  sincosq1lem  15979  sincosq1sgn  15980  sincosq2sgn  15981  sincosq3sgn  15982  sincosq4sgn  15983  sinq12gt0  15984  cosq14gt0  15986  cosq23lt0  15987  coseq0q4123  15988  coseq00topi  15989  coseq0negpitopi  15990  tangtx  15992  sincos4thpi  15994  tan4thpi  15995  sincos6thpi  15996  pigt3  15998  cosordlem  16003  cosq34lt1  16004  cos02pilt1  16005  cos0pilt1  16006  ioocosf1o  16008  negpitopissre  16009  log1  16020  loge  16021  2logb9irr  16129  sqrt2cxp2logb9e3  16133  2logb9irrap  16135  log2tlbndlog2  16142  log2ublem1  16143  log2ublem2  16144  log2ublem3  16145  log2ublog2  16146  birthdaylog2  16150  ppi1  16192  cht1  16193  ppi1i  16194  ppi2i  16195  cht2  16198  cht3  16199  chtqrpcl  16201  mpodvdsmulf1o  16206  fsumdvdsmul  16207  1sgm2ppw  16211  ppiublem1  16213  ppiublem2  16214  ppiqub  16215  chtqub  16218  bpos1lem  16231  lgsdir2lem2  16270  lgsdir2lem3  16271  lgseisenlem4  16314  2lgsoddprmlem3  16352  2sqlem9  16365  2sqlem10  16366  opvtxfvi  16390  opiedgfvi  16391  umgrbien  16473  usgrprc  16615  vtxdfifiun  16660  upgr2wlkdc  16740  konigsbergvtx  16845  konigsbergiedg  16846  konigsbergumgr  16850  konigsberglem1  16851  konigsberglem2  16852  konigsberglem3  16853  konigsberglem5  16855  konigsberg  16856  ex-fl  16861  ex-ceil  16862  ex-bc  16865  ex-dvds  16866  ex-gcd  16867  bj-charfunbi  16959  bj-unex  17067  bj-nn0suc0  17098  bj-nntrans  17099  bj-nnelirr  17101  012of  17145  2o01f  17146  pwle2  17150  nnsf  17170  peano3nninf  17172  exmidsbthrlem  17189  sbthom  17193  repiecelem  17196  repiecele0  17197  repiecege0  17198  isomninnlem  17201  iooref1o  17205  trilpolemisumle  17209  trilpolemeq1  17211  trilpolemlt1  17212  apdiff  17219  iswomninnlem  17221  iswomni0  17223  ismkvnnlem  17224  dceqnconst  17232  dcapnconst  17233  nconstwlpolemgt0  17236  taupi  17245