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  6538  tpostpos  6539  tpossym  6551  frecex  6669  frecfnom  6676  2oex  6708  sucinc  6722  fnoei  6729  oeiexg  6730  nnacli  6759  nnmcli  6760  elec  6852  ecovcom  6920  ecovass  6922  ecovdi  6924  fnmap  6933  mapval  6938  elmap  6962  elpm  6964  elpm2  6965  map0  6976  ixpconst  6995  entri  7078  endisj  7127  xpcomco  7129  phplem2  7159  1ndom2  7171  ssfiexmid  7183  domfiexmid  7187  exmidpw2en  7224  unfiexmid  7230  unfiin  7238  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  9729  halfnz  9754  9p1e10  9791  numnncl  9798  numltc  9819  le9lt10  9820  nummac  9838  8lt10  9925  7lt10  9926  6lt10  9927  5lt10  9928  4lt10  9929  3lt10  9930  2lt10  9931  1lt10  9932  eluzaddi  9966  eluzsubi  9967  uzuzle23  9979  uzuzle24  9980  uzuzle34  9981  eluz2nn  9983  eluz4eluz2  9985  eluzge3nn  9989  divfnzn  10038  elq  10039  qreccl  10059  xrltnr  10199  mnfltpnf  10205  xaddmnf1  10268  pnfaddmnf  10270  mnfaddpnf  10271  xrex  10276  xaddid1  10282  xsubge0  10301  xposdif  10302  xleaddadd  10307  elicc2i  10359  ioomax  10368  iccmax  10369  ioopos  10370  elxrge0  10398  iccshftri  10415  iccshftli  10417  iccdili  10419  icccntri  10421  unitssre  10426  fz10  10468  fz00m1  10469  fzpreddisj  10496  fz0to4untppr  10549  dfrp2  10716  fldiv4p1lem1div2  10762  fldiv4lem1div2  10764  frecfzennn  10885  xnn0nnen  10896  fnn0nninf  10897  fxnn0nninf  10898  0tonninf  10899  1tonninf  10900  m1expcl2  11020  m1expcl  11021  nn0expcli  11024  sqmuli  11081  cu2  11097  i3  11100  subsqi  11108  binom2subi  11114  bcpasc  11227  4bc2eq6  11236  hashinfom  11240  prhash2ex  11273  hashp1i  11274  lsw0g  11376  swrdccat3blem  11534  rei  11688  imi  11689  readdi  11717  imaddi  11718  remuli  11719  immuli  11720  cjaddi  11721  cjmuli  11722  ipcni  11723  crrei  11725  crimi  11726  rexfiuz  11778  sqrt1  11835  sqrt4  11836  sqrt9  11837  abs1  11861  sqrtmulii  11924  abslti  11928  abslei  11929  abssubi  11940  absmuli  11941  sqabsaddi  11942  sqabssubi  11943  abstrii  11945  fimaxre2  12017  fiidxsupcl  12019  climz  12084  abscn2  12107  recn2  12109  imcn2  12110  climabs  12112  climre  12114  climim  12115  fsumcnv  12230  fsumrelem  12264  fsumre  12265  fsumim  12266  arisum2  12292  expcnv  12297  geo2sum2  12308  geo2lim  12309  0.999...  12314  geoihalfsum  12315  fprodcnv  12418  fprodge0  12430  fprodge1  12432  ege2le3  12464  ef0  12465  reeff1  12493  tan0  12524  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  cos1bnd  12552  cos2bnd  12553  sinltxirr  12554  sin01gt0  12555  cos01gt0  12556  sin02gt0  12557  sincos1sgn  12558  sincos2sgn  12559  cos12dec  12561  egt2lt3  12573  epos  12574  ene1  12578  eap1  12579  3dvds  12657  3dvdsdec  12658  3dvds2dec  12659  odd2np1lem  12665  n2dvds1  12705  z4even  12709  ndvdsi  12726  flodddiv4  12729  bitsp1o  12746  0bits  12752  gcd0val  12763  6gcd4e2  12798  3lcm2e6woprm  12890  6lcm4e12  12891  3lcm2e6  12965  sqrt2irrlem  12966  phimullem  13033  pockthi  13167  4sqlem19  13218  dec2dvds  13220  dec5dvds2  13222  dec2nprm  13224  modxai  13225  mod2xnegi  13228  gcdi  13230  gcdmodi  13231  numexpp1  13234  karatsuba  13240  2exp7  13244  1259lem4  13275  1259lem5  13276  1259prm  13277  ballotfilemofi  13278  ballotfilem1  13279  ballotfilem2  13287  ballotfilemfmpn  13293  ballotfilemefi  13296  ballotfilemodife  13299  ballotfilem4  13300  ballotfilemiex  13303  ballotfilemimin  13308  ballotfilemic  13309  ballotfilemsval  13311  ballotfilemsdom  13314  ballotfilemsel1i  13315  ballotfilemsima  13318  ballotfilemrval  13320  ballotfilemfrceq  13331  ballotfilemfrcn0  13332  ballotfilem1ri  13337  ballotfilem7  13338  ballotfilem8  13339  ballotfilemth  13340  xpnnen  13344  xpomen  13345  ennnfonelemj0  13351  ennnfonelem0  13355  ennnfonelemhf1o  13363  exmidunben  13376  qnnen  13381  unct  13392  setscom  13451  strleun  13518  prdsvallem  13681  imasival  13687  ismgm  13737  fn0g  13755  fngzsum  13768  issgrp  13778  ismnddef  13791  isghm  14106  prdsex  14280  isrng  14341  rngmgpf  14344  isring  14412  mgpf  14423  dfrhm2  14571  rhmex  14574  isdomn  14688  rmodislmod  14798  lidlmex  14922  mopnset  14999  cnfldstr  15005  cnfldcj  15012  cnfld0  15018  cnfldplusf  15021  zringcrng  15037  zringmulr  15044  zringmpg  15051  znval  15081  psrval  15162  fnpsr  15163  fnmpl  15221  txtopi  15499  txunii  15502  upxp  15510  uptx  15512  cnmpt1st  15526  cnmpt2nd  15527  txswaphmeolem  15558  qtopbasss  15759  cnmet  15768  cnfldms  15774  cnopncntop  15782  cnopn  15783  remet  15786  blssioo  15791  tgqioo  15793  tgioo2cntop  15795  tgioo2  15797  divcnap  15803  abscncf  15823  recncf  15824  imcncf  15825  cjcncf  15826  mulc1cncf  15827  cncfcn1cntop  15832  idcncf  15839  cdivcncfap  15842  expcncf  15847  cnrehmeocntop  15848  maxcncf  15853  mincncf  15854  ivthreinc  15883  hovercncf  15884  limccnp2lem  15914  limccnp2cntop  15915  dvcnp2cntop  15937  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  dvrecap  15951  dveflem  15964  dvef  15965  sincn  16007  coscn  16008  reeff1oleme  16010  reeff1o  16011  cosz12  16019  sin0pilem1  16020  sin0pilem2  16021  pipos  16027  sinhalfpilem  16030  sincosq1lem  16064  sincosq1sgn  16065  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  sinq12gt0  16069  cosq14gt0  16071  cosq23lt0  16072  coseq0q4123  16073  coseq00topi  16074  coseq0negpitopi  16075  tangtx  16077  sincos4thpi  16079  tan4thpi  16080  sincos6thpi  16081  pigt3  16083  cosordlem  16089  cosq34lt1  16090  cos02pilt1  16091  cos0pilt1  16092  ioocosf1o  16094  negpitopissre  16095  log1  16107  loge  16108  2logb9irr  16219  sqrt2cxp2logb9e3  16223  2logb9irrap  16225  log2tlbndlog2  16232  log2ublem1  16233  log2ublem2  16234  log2ublem3  16235  log2ublog2  16236  birthdaylog2  16240  ppi1  16282  cht1  16283  ppi1i  16284  ppi2i  16285  cht2  16288  cht3  16289  chtqrpcl  16291  mpodvdsmulf1o  16296  fsumdvdsmul  16297  1sgm2ppw  16301  ppiublem1  16303  ppiublem2  16304  ppiqub  16305  chtqub  16308  bpos1lem  16321  bposlem6  16328  bposlem7  16329  bposlem8  16330  bposlem9  16331  lgsdir2lem2  16365  lgsdir2lem3  16366  lgseisenlem4  16409  2lgsoddprmlem3  16447  2sqlem9  16460  2sqlem10  16461  opvtxfvi  16485  opiedgfvi  16486  umgrbien  16568  usgrprc  16710  vtxdfifiun  16755  upgr2wlkdc  16835  konigsbergvtx  16940  konigsbergiedg  16941  konigsbergumgr  16945  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  konigsberglem5  16950  konigsberg  16951  ex-fl  16956  ex-ceil  16957  ex-bc  16960  ex-dvds  16961  ex-gcd  16962  bj-charfunbi  17054  bj-unex  17162  bj-nn0suc0  17193  bj-nntrans  17194  bj-nnelirr  17196  012of  17240  2o01f  17241  pwle2  17245  nnsf  17266  peano3nninf  17268  exmidsbthrlem  17285  sbthom  17289  repiecelem  17292  repiecele0  17293  repiecege0  17294  isomninnlem  17297  iooref1o  17301  trilpolemisumle  17306  trilpolemeq1  17308  trilpolemlt1  17309  apdiff  17316  iswomninnlem  17318  iswomni0  17320  ismkvnnlem  17321  dceqnconst  17329  dcapnconst  17330  nconstwlpolemgt0  17333  taupi  17342