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 ⊢ 𝜒

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  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  3732  ralpr  3763  rexpr  3764  preq12i  3792  dfop  3901  opeq12i  3907  breq12i  4137  mpteq2ia  4215  exmidundif  4341  exmidundifim  4342  opex  4367  opi2  4371  opth2  4378  opeqsn  4391  opeqpr  4392  uniop  4394  opelopaba  4406  braba  4407  opelopab  4412  brab  4413  opelopabaf  4414  unex  4585  snnex  4592  op1stb  4622  ifelpwun  4627  ifex  4630  onun2i  4636  onsucssi  4651  ontriexmidim  4667  ontr2exmid  4670  onsucsssucexmid  4672  onsucelsucexmid  4675  opthreg  4701  tfis  4728  finds  4745  finds2  4746  nnregexmid  4766  xpeq12i  4794  opelvv  4823  eqrelriiv  4867  eqrelrdv  4869  xpss  4881  xpex  4889  relop  4928  brco  4949  opelcnv  4960  brcnv  4961  asymref  5171  codir  5174  ssrnres  5228  dmprop  5260  dfco2  5285  cossxp  5308  cocnvss  5311  coex  5331  funsn  5427  fnsn  5433  feq23i  5526  resasplitss  5567  fabex  5578  fvex  5713  xpsn  5879  fmptap  5899  opabex  5935  rinvf1o  6029  acexmidlemv  6077  oveq12i  6091  oprabid  6111  oprabss  6168  caovcom  6241  opabex3  6345  iunex  6346  oprabex  6355  ofmres  6363  op1st  6374  op2nd  6375  fo1st  6385  fo2nd  6386  mpoex  6444  1stconst  6451  2ndconst  6452  algrflem  6459  dftpos4  6528  tpostpos  6529  tpossym  6541  frecex  6659  frecfnom  6666  2oex  6698  sucinc  6712  fnoei  6719  oeiexg  6720  nnacli  6749  nnmcli  6750  elec  6842  ecovcom  6910  ecovass  6912  ecovdi  6914  fnmap  6923  mapval  6928  elmap  6952  elpm  6954  elpm2  6955  map0  6965  ixpconst  6984  entri  7067  endisj  7116  xpcomco  7118  phplem2  7148  1ndom2  7160  ssfiexmid  7172  domfiexmid  7176  exmidpw2en  7213  unfiexmid  7219  unfiin  7227  inresflem  7394  casefun  7419  caserel  7421  caseinj  7423  omp1eomlem  7428  omp1eom  7429  endjusym  7430  djufun  7438  djuinj  7440  ctssdccl  7445  ctssdclemr  7446  nninfex  7455  infnninf  7458  fodjuomnilemdc  7478  ctssexmid  7484  exmidonfinlem  7539  dju1p1e2  7543  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  exmidaclem  7558  pw1dom2  7580  onntri35  7590  onntri45  7594  2oneel  7616  2omotaplemst  7618  acnccim  7632  1lt2pi  7701  indpi  7703  1nq  7727  rec1nq  7756  1lt2nq  7767  ltaddnq  7768  halfnqq  7771  prarloclemarch2  7780  prarloclemlt  7854  prarloclemcalc  7863  genpelxp  7872  ltexprlempr  7969  recexprlempr  7993  cauappcvgprlemcl  8014  cauappcvgprlemladd  8019  caucvgprlemcl  8037  caucvgprprlemcl  8065  suplocexprlemell  8074  suplocexprlemdisj  8081  suplocexprlemub  8084  0r  8111  1sr  8112  m1r  8113  m1p1sr  8121  m1m1sr  8122  0lt1sr  8126  1ne0sr  8127  1idsr  8129  recexgt0sr  8134  prsradd  8147  caucvgsrlemoffres  8161  caucvgsr  8163  mappsrprg  8165  map2psrprg  8166  pitonnlem1p1  8207  pitonnlem2  8208  pitoregt0  8210  peano2nnnn  8214  axi2m1  8236  axprecex  8241  axcnre  8242  nnindnn  8254  nntopi  8255  0cn  8312  addcli  8324  mulcli  8325  mulcomi  8326  readdcli  8333  remulcli  8334  rexpssxrxp  8364  ltrelxr  8380  gtneii  8415  lttri3i  8417  letri3i  8418  ltnsymi  8419  lenlti  8420  ltlei  8421  mulgt0i  8429  mulgt0ii  8430  0lt1  8447  addcomi  8464  pncan3oi  8536  resubcli  8583  subcli  8596  pncan3i  8597  negsubi  8598  subnegi  8599  subeq0i  8600  neg11i  8601  negcon1i  8602  negcon2i  8603  mulneg1i  8725  mulneg2i  8726  mul2negi  8727  addgt0ii  8813  ltnegi  8815  lenegi  8816  ltnegcon2i  8817  lesub0i  8818  ltaddposi  8819  posdifi  8820  ltnegcon1i  8821  lenegcon1i  8822  subge0i  8823  1ap0  8912  ltapii  8957  recrecapi  9068  dividapi  9069  div0api  9070  rec11apii  9085  divdiv32api  9091  recgt0ii  9231  ltrecii  9242  ltdiv23ii  9251  sup3exmid  9281  nnssre  9291  nnind  9303  nnmulcli  9309  nnsubi  9327  0le2  9377  1lt3  9459  2lt4  9461  1lt4  9462  3lt5  9464  2lt5  9465  1lt5  9466  4lt6  9468  3lt6  9469  2lt6  9470  1lt6  9471  5lt7  9473  4lt7  9474  3lt7  9475  2lt7  9476  1lt7  9477  6lt8  9479  5lt8  9480  4lt8  9481  3lt8  9482  2lt8  9483  1lt8  9484  7lt9  9486  6lt9  9487  5lt9  9488  4lt9  9489  3lt9  9490  2lt9  9491  1lt9  9492  2muline0  9513  nn0addcli  9583  nn0mulcli  9584  nn0addge1i  9594  nn0addge2i  9595  dfz2  9700  halfnz  9725  9p1e10  9762  numnncl  9769  numltc  9785  le9lt10  9786  nummac  9804  8lt10  9891  7lt10  9892  6lt10  9893  5lt10  9894  4lt10  9895  3lt10  9896  2lt10  9897  1lt10  9898  eluzaddi  9932  eluzsubi  9933  uzuzle23  9945  uzuzle24  9946  uzuzle34  9947  eluz2nn  9949  eluz4eluz2  9951  eluzge3nn  9955  divfnzn  10004  elq  10005  qreccl  10025  xrltnr  10164  mnfltpnf  10170  xaddmnf1  10233  pnfaddmnf  10235  mnfaddpnf  10236  xrex  10241  xaddid1  10247  xsubge0  10266  xposdif  10267  xleaddadd  10272  elicc2i  10324  ioomax  10333  iccmax  10334  ioopos  10335  elxrge0  10363  iccshftri  10380  iccshftli  10382  iccdili  10384  icccntri  10386  unitssre  10391  fz10  10433  fz00m1  10434  fzpreddisj  10461  fz0to4untppr  10514  dfrp2  10681  fldiv4p1lem1div2  10723  fldiv4lem1div2  10725  frecfzennn  10846  xnn0nnen  10857  fnn0nninf  10858  fxnn0nninf  10859  0tonninf  10860  1tonninf  10861  m1expcl2  10981  m1expcl  10982  nn0expcli  10985  sqmuli  11042  cu2  11058  i3  11061  subsqi  11069  binom2subi  11075  bcpasc  11187  4bc2eq6  11196  hashinfom  11200  prhash2ex  11233  hashp1i  11234  lsw0g  11336  swrdccat3blem  11494  rei  11648  imi  11649  readdi  11677  imaddi  11678  remuli  11679  immuli  11680  cjaddi  11681  cjmuli  11682  ipcni  11683  crrei  11685  crimi  11686  rexfiuz  11738  sqrt1  11795  sqrt4  11796  sqrt9  11797  abs1  11821  sqrtmulii  11883  abslti  11887  abslei  11888  abssubi  11899  absmuli  11900  sqabsaddi  11901  sqabssubi  11902  abstrii  11904  fimaxre2  11976  climz  12041  abscn2  12064  recn2  12066  imcn2  12067  climabs  12069  climre  12071  climim  12072  fsumcnv  12187  fsumrelem  12221  fsumre  12222  fsumim  12223  arisum2  12249  expcnv  12254  geo2sum2  12265  geo2lim  12266  0.999...  12271  geoihalfsum  12272  fprodcnv  12375  fprodge0  12387  fprodge1  12389  ege2le3  12421  ef0  12422  reeff1  12450  tan0  12481  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  cos1bnd  12509  cos2bnd  12510  sinltxirr  12511  sin01gt0  12512  cos01gt0  12513  sin02gt0  12514  sincos1sgn  12515  sincos2sgn  12516  cos12dec  12518  egt2lt3  12530  epos  12531  ene1  12535  eap1  12536  3dvds  12614  3dvdsdec  12615  3dvds2dec  12616  odd2np1lem  12622  n2dvds1  12662  z4even  12666  ndvdsi  12683  flodddiv4  12686  bitsp1o  12703  0bits  12709  gcd0val  12720  6gcd4e2  12755  3lcm2e6woprm  12847  6lcm4e12  12848  3lcm2e6  12921  sqrt2irrlem  12922  phimullem  12986  pockthi  13120  4sqlem19  13171  dec2dvds  13173  dec5dvds2  13175  dec2nprm  13177  modxai  13178  gcdi  13182  gcdmodi  13183  numexpp1  13186  karatsuba  13192  2exp7  13196  ballotfilemofi  13202  ballotfilem1  13203  ballotfilem2  13211  ballotfilemfmpn  13217  ballotfilemefi  13220  ballotfilemodife  13223  ballotfilem4  13224  ballotfilemiex  13227  ballotfilemimin  13232  ballotfilemic  13233  ballotfilemsval  13235  ballotfilemsdom  13238  ballotfilemsel1i  13239  ballotfilemsima  13242  ballotfilemrval  13244  ballotfilemfrceq  13255  ballotfilemfrcn0  13256  ballotfilem1ri  13261  ballotfilem7  13262  ballotfilem8  13263  ballotfilemth  13264  xpnnen  13268  xpomen  13269  ennnfonelemj0  13275  ennnfonelem0  13279  ennnfonelemhf1o  13287  exmidunben  13300  qnnen  13305  unct  13316  setscom  13375  strleun  13441  prdsvallem  13604  imasival  13610  ismgm  13660  fn0g  13678  fngzsum  13691  issgrp  13701  ismnddef  13714  isghm  14029  prdsex  14155  isrng  14216  rngmgpf  14219  isring  14287  mgpf  14298  dfrhm2  14444  rhmex  14447  isdomn  14561  rmodislmod  14671  lidlmex  14795  mopnset  14872  cnfldstr  14878  cnfldcj  14885  cnfld0  14891  cnfldplusf  14894  zringcrng  14910  zringmulr  14917  zringmpg  14924  znval  14954  psrval  15033  fnpsr  15034  fnmpl  15067  txtopi  15345  txunii  15348  upxp  15356  uptx  15358  cnmpt1st  15372  cnmpt2nd  15373  txswaphmeolem  15404  qtopbasss  15605  cnmet  15614  cnfldms  15620  cnopncntop  15628  cnopn  15629  remet  15632  blssioo  15637  tgqioo  15639  tgioo2cntop  15641  tgioo2  15643  divcnap  15649  abscncf  15669  recncf  15670  imcncf  15671  cjcncf  15672  mulc1cncf  15673  cncfcn1cntop  15678  idcncf  15685  cdivcncfap  15688  expcncf  15693  cnrehmeocntop  15694  maxcncf  15699  mincncf  15700  ivthreinc  15729  hovercncf  15730  limccnp2lem  15760  limccnp2cntop  15761  dvcnp2cntop  15783  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvrecap  15797  dveflem  15810  dvef  15811  sincn  15853  coscn  15854  reeff1oleme  15856  reeff1o  15857  cosz12  15864  sin0pilem1  15865  sin0pilem2  15866  pipos  15872  sinhalfpilem  15875  sincosq1lem  15909  sincosq1sgn  15910  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  sinq12gt0  15914  cosq14gt0  15916  cosq23lt0  15917  coseq0q4123  15918  coseq00topi  15919  coseq0negpitopi  15920  tangtx  15922  sincos4thpi  15924  tan4thpi  15925  sincos6thpi  15926  pigt3  15928  cosordlem  15933  cosq34lt1  15934  cos02pilt1  15935  cos0pilt1  15936  ioocosf1o  15938  negpitopissre  15939  log1  15950  loge  15951  2logb9irr  16056  sqrt2cxp2logb9e3  16060  2logb9irrap  16062  log2tlbndlog2  16065  log2ublem1  16066  log2ublem2  16067  log2ublem3  16068  log2ublog2  16069  birthdaylog2  16073  mpodvdsmulf1o  16087  fsumdvdsmul  16088  1sgm2ppw  16092  lgsdir2lem2  16131  lgsdir2lem3  16132  lgseisenlem4  16175  2lgsoddprmlem3  16213  2sqlem9  16226  2sqlem10  16227  opvtxfvi  16251  opiedgfvi  16252  umgrbien  16334  usgrprc  16476  vtxdfifiun  16521  upgr2wlkdc  16601  konigsbergvtx  16706  konigsbergiedg  16707  konigsbergumgr  16711  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  konigsberglem5  16716  konigsberg  16717  ex-fl  16722  ex-ceil  16723  ex-bc  16726  ex-dvds  16727  ex-gcd  16728  bj-charfunbi  16820  bj-unex  16928  bj-nn0suc0  16959  bj-nntrans  16960  bj-nnelirr  16962  012of  17006  2o01f  17007  pwle2  17011  nnsf  17022  peano3nninf  17024  exmidsbthrlem  17041  sbthom  17045  repiecelem  17048  repiecele0  17049  repiecege0  17050  isomninnlem  17053  iooref1o  17057  trilpolemisumle  17061  trilpolemeq1  17063  trilpolemlt1  17064  apdiff  17071  iswomninnlem  17073  iswomni0  17075  ismkvnnlem  17076  dceqnconst  17084  dcapnconst  17085  nconstwlpolemgt0  17088  taupi  17097