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  10755  fldiv4lem1div2  10757  frecfzennn  10878  xnn0nnen  10889  fnn0nninf  10890  fxnn0nninf  10891  0tonninf  10892  1tonninf  10893  m1expcl2  11013  m1expcl  11014  nn0expcli  11017  sqmuli  11074  cu2  11090  i3  11093  subsqi  11101  binom2subi  11107  bcpasc  11220  4bc2eq6  11229  hashinfom  11233  prhash2ex  11266  hashp1i  11267  lsw0g  11369  swrdccat3blem  11527  rei  11681  imi  11682  readdi  11710  imaddi  11711  remuli  11712  immuli  11713  cjaddi  11714  cjmuli  11715  ipcni  11716  crrei  11718  crimi  11719  rexfiuz  11771  sqrt1  11828  sqrt4  11829  sqrt9  11830  abs1  11854  sqrtmulii  11917  abslti  11921  abslei  11922  abssubi  11933  absmuli  11934  sqabsaddi  11935  sqabssubi  11936  abstrii  11938  fimaxre2  12010  fiidxsupcl  12012  climz  12077  abscn2  12100  recn2  12102  imcn2  12103  climabs  12105  climre  12107  climim  12108  fsumcnv  12223  fsumrelem  12257  fsumre  12258  fsumim  12259  arisum2  12285  expcnv  12290  geo2sum2  12301  geo2lim  12302  0.999...  12307  geoihalfsum  12308  fprodcnv  12411  fprodge0  12423  fprodge1  12425  ege2le3  12457  ef0  12458  reeff1  12486  tan0  12517  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  sinltxirr  12547  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  sincos1sgn  12551  sincos2sgn  12552  cos12dec  12554  egt2lt3  12566  epos  12567  ene1  12571  eap1  12572  3dvds  12650  3dvdsdec  12651  3dvds2dec  12652  odd2np1lem  12658  n2dvds1  12698  z4even  12702  ndvdsi  12719  flodddiv4  12722  bitsp1o  12739  0bits  12745  gcd0val  12756  6gcd4e2  12791  3lcm2e6woprm  12883  6lcm4e12  12884  3lcm2e6  12958  sqrt2irrlem  12959  phimullem  13026  pockthi  13160  4sqlem19  13211  dec2dvds  13213  dec5dvds2  13215  dec2nprm  13217  modxai  13218  mod2xnegi  13221  gcdi  13223  gcdmodi  13224  numexpp1  13227  karatsuba  13233  2exp7  13237  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilemofi  13271  ballotfilem1  13272  ballotfilem2  13280  ballotfilemfmpn  13286  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilem4  13293  ballotfilemiex  13296  ballotfilemimin  13301  ballotfilemic  13302  ballotfilemsval  13304  ballotfilemsdom  13307  ballotfilemsel1i  13308  ballotfilemsima  13311  ballotfilemrval  13313  ballotfilemfrceq  13324  ballotfilemfrcn0  13325  ballotfilem1ri  13330  ballotfilem7  13331  ballotfilem8  13332  ballotfilemth  13333  xpnnen  13337  xpomen  13338  ennnfonelemj0  13344  ennnfonelem0  13348  ennnfonelemhf1o  13356  exmidunben  13369  qnnen  13374  unct  13385  setscom  13444  strleun  13511  prdsvallem  13674  imasival  13680  ismgm  13730  fn0g  13748  fngzsum  13761  issgrp  13771  ismnddef  13784  isghm  14099  prdsex  14263  isrng  14324  rngmgpf  14327  isring  14395  mgpf  14406  dfrhm2  14552  rhmex  14555  isdomn  14669  rmodislmod  14779  lidlmex  14903  mopnset  14980  cnfldstr  14986  cnfldcj  14993  cnfld0  14999  cnfldplusf  15002  zringcrng  15018  zringmulr  15025  zringmpg  15032  znval  15062  psrval  15141  fnpsr  15142  fnmpl  15183  txtopi  15461  txunii  15464  upxp  15472  uptx  15474  cnmpt1st  15488  cnmpt2nd  15489  txswaphmeolem  15520  qtopbasss  15721  cnmet  15730  cnfldms  15736  cnopncntop  15744  cnopn  15745  remet  15748  blssioo  15753  tgqioo  15755  tgioo2cntop  15757  tgioo2  15759  divcnap  15765  abscncf  15785  recncf  15786  imcncf  15787  cjcncf  15788  mulc1cncf  15789  cncfcn1cntop  15794  idcncf  15801  cdivcncfap  15804  expcncf  15809  cnrehmeocntop  15810  maxcncf  15815  mincncf  15816  ivthreinc  15845  hovercncf  15846  limccnp2lem  15876  limccnp2cntop  15877  dvcnp2cntop  15899  dvaddxxbr  15901  dvmulxxbr  15902  dvcoapbr  15907  dvrecap  15913  dveflem  15926  dvef  15927  sincn  15969  coscn  15970  reeff1oleme  15972  reeff1o  15973  cosz12  15981  sin0pilem1  15982  sin0pilem2  15983  pipos  15989  sinhalfpilem  15992  sincosq1lem  16026  sincosq1sgn  16027  sincosq2sgn  16028  sincosq3sgn  16029  sincosq4sgn  16030  sinq12gt0  16031  cosq14gt0  16033  cosq23lt0  16034  coseq0q4123  16035  coseq00topi  16036  coseq0negpitopi  16037  tangtx  16039  sincos4thpi  16041  tan4thpi  16042  sincos6thpi  16043  pigt3  16045  cosordlem  16051  cosq34lt1  16052  cos02pilt1  16053  cos0pilt1  16054  ioocosf1o  16056  negpitopissre  16057  log1  16069  loge  16070  2logb9irr  16181  sqrt2cxp2logb9e3  16185  2logb9irrap  16187  log2tlbndlog2  16194  log2ublem1  16195  log2ublem2  16196  log2ublem3  16197  log2ublog2  16198  birthdaylog2  16202  ppi1  16244  cht1  16245  ppi1i  16246  ppi2i  16247  cht2  16250  cht3  16251  chtqrpcl  16253  mpodvdsmulf1o  16258  fsumdvdsmul  16259  1sgm2ppw  16263  ppiublem1  16265  ppiublem2  16266  ppiqub  16267  chtqub  16270  bpos1lem  16283  bposlem6  16290  bposlem7  16291  bposlem8  16292  bposlem9  16293  lgsdir2lem2  16327  lgsdir2lem3  16328  lgseisenlem4  16371  2lgsoddprmlem3  16409  2sqlem9  16422  2sqlem10  16423  opvtxfvi  16447  opiedgfvi  16448  umgrbien  16530  usgrprc  16672  vtxdfifiun  16717  upgr2wlkdc  16797  konigsbergvtx  16902  konigsbergiedg  16903  konigsbergumgr  16907  konigsberglem1  16908  konigsberglem2  16909  konigsberglem3  16910  konigsberglem5  16912  konigsberg  16913  ex-fl  16918  ex-ceil  16919  ex-bc  16922  ex-dvds  16923  ex-gcd  16924  bj-charfunbi  17016  bj-unex  17124  bj-nn0suc0  17155  bj-nntrans  17156  bj-nnelirr  17158  012of  17202  2o01f  17203  pwle2  17207  nnsf  17227  peano3nninf  17229  exmidsbthrlem  17246  sbthom  17250  repiecelem  17253  repiecele0  17254  repiecege0  17255  isomninnlem  17258  iooref1o  17262  trilpolemisumle  17267  trilpolemeq1  17269  trilpolemlt1  17270  apdiff  17277  iswomninnlem  17279  iswomni0  17281  ismkvnnlem  17282  dceqnconst  17290  dcapnconst  17291  nconstwlpolemgt0  17294  taupi  17303