Theorem mp2an 426

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 424	. 2 ⊢ (𝜓 → 𝜒)
5	1, 4	ax-mp 5	1 ⊢ 𝜒

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mp4an  427  jaoi  724  mp3an  1374  barbara  2181  eqeq12i  2248  el2v  2821  vtocl2  2872  spc2ev  2915  sbc2ie  3117  csbieb  3183  sseq12i  3270  uneq12i  3375  ineq12i  3424  ifssun  3641  nelpri  3718  ralpr  3749  rexpr  3750  preq12i  3778  dfop  3887  opeq12i  3893  breq12i  4123  mpteq2ia  4201  exmidundif  4324  exmidundifim  4325  opex  4350  opi2  4354  opth2  4361  opeqsn  4374  opeqpr  4375  uniop  4377  opelopaba  4389  braba  4390  opelopab  4395  brab  4396  opelopabaf  4397  unex  4567  snnex  4574  op1stb  4604  ifelpwun  4609  ifex  4612  onun2i  4618  onsucssi  4633  ontriexmidim  4649  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmid  4657  opthreg  4683  tfis  4710  finds  4727  finds2  4728  nnregexmid  4748  xpeq12i  4776  opelvv  4805  eqrelriiv  4849  eqrelrdv  4851  xpss  4863  xpex  4871  relop  4910  brco  4931  opelcnv  4942  brcnv  4943  asymref  5153  codir  5156  ssrnres  5210  dmprop  5242  dfco2  5267  cossxp  5290  cocnvss  5293  coex  5313  funsn  5409  fnsn  5415  feq23i  5508  resasplitss  5549  fabex  5560  fvex  5695  xpsn  5859  fmptap  5879  opabex  5915  rinvf1o  6008  acexmidlemv  6056  oveq12i  6070  oprabid  6090  oprabss  6147  caovcom  6220  opabex3  6324  iunex  6325  oprabex  6334  ofmres  6342  op1st  6353  op2nd  6354  fo1st  6364  fo2nd  6365  mpoex  6423  1stconst  6430  2ndconst  6431  algrflem  6438  dftpos4  6507  tpostpos  6508  tpossym  6520  frecex  6638  frecfnom  6645  2oex  6677  sucinc  6691  fnoei  6698  oeiexg  6699  nnacli  6728  nnmcli  6729  elec  6821  ecovcom  6889  ecovass  6891  ecovdi  6893  fnmap  6902  mapval  6907  elmap  6924  elpm  6926  elpm2  6927  map0  6937  ixpconst  6956  entri  7039  endisj  7088  xpcomco  7090  phplem2  7120  1ndom2  7132  ssfiexmid  7144  domfiexmid  7148  exmidpw2en  7185  unfiexmid  7191  unfiin  7199  inresflem  7364  casefun  7389  caserel  7391  caseinj  7393  omp1eomlem  7398  omp1eom  7399  endjusym  7400  djufun  7408  djuinj  7410  ctssdccl  7415  ctssdclemr  7416  nninfex  7425  infnninf  7428  fodjuomnilemdc  7448  ctssexmid  7454  exmidonfinlem  7509  dju1p1e2  7513  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  pw1dom2  7550  onntri35  7560  onntri45  7564  2oneel  7586  2omotaplemst  7588  acnccim  7602  1lt2pi  7671  indpi  7673  1nq  7697  rec1nq  7726  1lt2nq  7737  ltaddnq  7738  halfnqq  7741  prarloclemarch2  7750  prarloclemlt  7824  prarloclemcalc  7833  genpelxp  7842  ltexprlempr  7939  recexprlempr  7963  cauappcvgprlemcl  7984  cauappcvgprlemladd  7989  caucvgprlemcl  8007  caucvgprprlemcl  8035  suplocexprlemell  8044  suplocexprlemdisj  8051  suplocexprlemub  8054  0r  8081  1sr  8082  m1r  8083  m1p1sr  8091  m1m1sr  8092  0lt1sr  8096  1ne0sr  8097  1idsr  8099  recexgt0sr  8104  prsradd  8117  caucvgsrlemoffres  8131  caucvgsr  8133  mappsrprg  8135  map2psrprg  8136  pitonnlem1p1  8177  pitonnlem2  8178  pitoregt0  8180  peano2nnnn  8184  axi2m1  8206  axprecex  8211  axcnre  8212  nnindnn  8224  nntopi  8225  0cn  8282  addcli  8294  mulcli  8295  mulcomi  8296  readdcli  8303  remulcli  8304  rexpssxrxp  8334  ltrelxr  8350  gtneii  8385  lttri3i  8387  letri3i  8388  ltnsymi  8389  lenlti  8390  ltlei  8391  mulgt0i  8399  mulgt0ii  8400  0lt1  8417  addcomi  8434  pncan3oi  8506  resubcli  8553  subcli  8566  pncan3i  8567  negsubi  8568  subnegi  8569  subeq0i  8570  neg11i  8571  negcon1i  8572  negcon2i  8573  mulneg1i  8695  mulneg2i  8696  mul2negi  8697  addgt0ii  8783  ltnegi  8785  lenegi  8786  ltnegcon2i  8787  lesub0i  8788  ltaddposi  8789  posdifi  8790  ltnegcon1i  8791  lenegcon1i  8792  subge0i  8793  1ap0  8882  ltapii  8927  recrecapi  9038  dividapi  9039  div0api  9040  rec11apii  9055  divdiv32api  9061  recgt0ii  9201  ltrecii  9212  ltdiv23ii  9221  sup3exmid  9251  nnssre  9261  nnind  9273  nnmulcli  9279  nnsubi  9297  0le2  9347  1lt3  9429  2lt4  9431  1lt4  9432  3lt5  9434  2lt5  9435  1lt5  9436  4lt6  9438  3lt6  9439  2lt6  9440  1lt6  9441  5lt7  9443  4lt7  9444  3lt7  9445  2lt7  9446  1lt7  9447  6lt8  9449  5lt8  9450  4lt8  9451  3lt8  9452  2lt8  9453  1lt8  9454  7lt9  9456  6lt9  9457  5lt9  9458  4lt9  9459  3lt9  9460  2lt9  9461  1lt9  9462  2muline0  9483  nn0addcli  9553  nn0mulcli  9554  nn0addge1i  9564  nn0addge2i  9565  dfz2  9670  halfnz  9695  9p1e10  9732  numnncl  9739  numltc  9755  le9lt10  9756  nummac  9774  8lt10  9861  7lt10  9862  6lt10  9863  5lt10  9864  4lt10  9865  3lt10  9866  2lt10  9867  1lt10  9868  eluzaddi  9902  eluzsubi  9903  uzuzle23  9915  uzuzle24  9916  uzuzle34  9917  eluz2nn  9919  eluz4eluz2  9921  eluzge3nn  9925  divfnzn  9974  elq  9975  qreccl  9995  xrltnr  10134  mnfltpnf  10140  xaddmnf1  10203  pnfaddmnf  10205  mnfaddpnf  10206  xrex  10211  xaddid1  10217  xsubge0  10236  xposdif  10237  xleaddadd  10242  elicc2i  10294  ioomax  10303  iccmax  10304  ioopos  10305  elxrge0  10333  iccshftri  10350  iccshftli  10352  iccdili  10354  icccntri  10356  unitssre  10361  fz10  10403  fzpreddisj  10430  fz0to4untppr  10483  dfrp2  10650  fldiv4p1lem1div2  10692  fldiv4lem1div2  10694  frecfzennn  10815  xnn0nnen  10826  fnn0nninf  10827  fxnn0nninf  10828  0tonninf  10829  1tonninf  10830  m1expcl2  10950  m1expcl  10951  nn0expcli  10954  sqmuli  11011  cu2  11027  i3  11030  subsqi  11038  binom2subi  11044  bcpasc  11156  4bc2eq6  11165  hashinfom  11169  prhash2ex  11202  hashp1i  11203  lsw0g  11301  swrdccat3blem  11459  rei  11612  imi  11613  readdi  11641  imaddi  11642  remuli  11643  immuli  11644  cjaddi  11645  cjmuli  11646  ipcni  11647  crrei  11649  crimi  11650  rexfiuz  11702  sqrt1  11759  sqrt4  11760  sqrt9  11761  abs1  11785  sqrtmulii  11847  abslti  11851  abslei  11852  abssubi  11863  absmuli  11864  sqabsaddi  11865  sqabssubi  11866  abstrii  11868  fimaxre2  11940  climz  12005  abscn2  12028  recn2  12030  imcn2  12031  climabs  12033  climre  12035  climim  12036  fsumcnv  12151  fsumrelem  12185  fsumre  12186  fsumim  12187  arisum2  12213  expcnv  12218  geo2sum2  12229  geo2lim  12230  0.999...  12235  geoihalfsum  12236  fprodcnv  12339  fprodge0  12351  fprodge1  12353  ege2le3  12385  ef0  12386  reeff1  12414  tan0  12445  ef01bndlem  12470  sin01bnd  12471  cos01bnd  12472  cos1bnd  12473  cos2bnd  12474  sinltxirr  12475  sin01gt0  12476  cos01gt0  12477  sin02gt0  12478  sincos1sgn  12479  sincos2sgn  12480  cos12dec  12482  egt2lt3  12494  epos  12495  ene1  12499  eap1  12500  3dvds  12578  3dvdsdec  12579  3dvds2dec  12580  odd2np1lem  12586  n2dvds1  12626  z4even  12630  ndvdsi  12647  flodddiv4  12650  bitsp1o  12667  0bits  12673  gcd0val  12684  6gcd4e2  12719  3lcm2e6woprm  12811  6lcm4e12  12812  3lcm2e6  12885  sqrt2irrlem  12886  phimullem  12950  pockthi  13084  4sqlem19  13135  dec2dvds  13137  dec5dvds2  13139  dec2nprm  13141  modxai  13142  gcdi  13146  gcdmodi  13147  numexpp1  13150  karatsuba  13156  2exp7  13160  ballotfilemofi  13166  ballotfilem1  13167  ballotfilem2  13175  ballotfilemfmpn  13181  ballotfilemefi  13184  ballotfilemodife  13187  ballotfilem4  13188  ballotfilemiex  13191  ballotfilemimin  13196  ballotfilemic  13197  ballotfilemsval  13199  ballotfilemsdom  13202  ballotfilemsel1i  13203  ballotfilemsima  13206  ballotfilemrval  13208  ballotfilemfrceq  13219  ballotfilemfrcn0  13220  ballotfilem1ri  13225  ballotfilem7  13226  ballotfilem8  13227  ballotfilemth  13228  xpnnen  13232  xpomen  13233  ennnfonelemj0  13239  ennnfonelem0  13243  ennnfonelemhf1o  13251  exmidunben  13264  qnnen  13269  unct  13280  setscom  13339  strleun  13404  prdsvallem  13567  imasival  13573  ismgm  13623  fn0g  13641  fngsum  13654  issgrp  13669  ismnddef  13682  isghm  13999  prdsex  14117  isrng  14176  rngmgpf  14179  isring  14246  mgpf  14257  dfrhm2  14402  rhmex  14405  isdomn  14519  rmodislmod  14628  lidlmex  14752  mopnset  14829  cnfldstr  14835  cnfldcj  14842  cnfld0  14848  cnfldplusf  14851  zringcrng  14869  zringmulr  14876  zringmpg  14883  znval  14913  psrval  14943  fnpsr  14944  fnmpl  14977  txtopi  15255  txunii  15258  upxp  15266  uptx  15268  cnmpt1st  15282  cnmpt2nd  15283  txswaphmeolem  15314  qtopbasss  15515  cnmet  15524  cnfldms  15530  cnopncntop  15538  cnopn  15539  remet  15542  blssioo  15547  tgqioo  15549  tgioo2cntop  15551  tgioo2  15553  divcnap  15559  abscncf  15579  recncf  15580  imcncf  15581  cjcncf  15582  mulc1cncf  15583  cncfcn1cntop  15588  idcncf  15595  cdivcncfap  15598  expcncf  15603  cnrehmeocntop  15604  maxcncf  15609  mincncf  15610  ivthreinc  15639  hovercncf  15640  limccnp2lem  15670  limccnp2cntop  15671  dvcnp2cntop  15693  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  dvrecap  15707  dveflem  15720  dvef  15721  sincn  15763  coscn  15764  reeff1oleme  15766  reeff1o  15767  cosz12  15774  sin0pilem1  15775  sin0pilem2  15776  pipos  15782  sinhalfpilem  15785  sincosq1lem  15819  sincosq1sgn  15820  sincosq2sgn  15821  sincosq3sgn  15822  sincosq4sgn  15823  sinq12gt0  15824  cosq14gt0  15826  cosq23lt0  15827  coseq0q4123  15828  coseq00topi  15829  coseq0negpitopi  15830  tangtx  15832  sincos4thpi  15834  tan4thpi  15835  sincos6thpi  15836  pigt3  15838  cosordlem  15843  cosq34lt1  15844  cos02pilt1  15845  cos0pilt1  15846  ioocosf1o  15848  negpitopissre  15849  log1  15860  loge  15861  2logb9irr  15965  sqrt2cxp2logb9e3  15969  2logb9irrap  15971  mpodvdsmulf1o  15987  fsumdvdsmul  15988  1sgm2ppw  15992  lgsdir2lem2  16031  lgsdir2lem3  16032  lgseisenlem4  16075  2lgsoddprmlem3  16113  2sqlem9  16126  2sqlem10  16127  opvtxfvi  16151  opiedgfvi  16152  umgrbien  16234  usgrprc  16376  vtxdfifiun  16421  upgr2wlkdc  16501  konigsbergvtx  16606  konigsbergiedg  16607  konigsbergumgr  16611  konigsberglem1  16612  konigsberglem2  16613  konigsberglem3  16614  konigsberglem5  16616  konigsberg  16617  ex-fl  16622  ex-ceil  16623  ex-bc  16626  ex-dvds  16627  ex-gcd  16628  bj-charfunbi  16720  bj-unex  16828  bj-nn0suc0  16859  bj-nntrans  16860  bj-nnelirr  16862  012of  16906  2o01f  16907  pwle2  16911  nnsf  16922  peano3nninf  16924  exmidsbthrlem  16941  sbthom  16945  repiecelem  16948  repiecele0  16949  repiecege0  16950  isomninnlem  16953  iooref1o  16957  trilpolemisumle  16961  trilpolemeq1  16963  trilpolemlt1  16964  apdiff  16971  iswomninnlem  16973  iswomni0  16975  ismkvnnlem  16976  dceqnconst  16985  dcapnconst  16986  nconstwlpolemgt0  16989  taupi  16998