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  717  mp3an  1348  barbara  2143  eqeq12i  2210  vtocl2  2819  spc2ev  2860  sbc2ie  3061  csbieb  3126  sseq12i  3211  uneq12i  3315  ineq12i  3362  ifssun  3575  nelpri  3646  ralpr  3677  rexpr  3678  preq12i  3704  dfop  3807  opeq12i  3813  breq12i  4042  mpteq2ia  4119  exmidundif  4239  exmidundifim  4240  opex  4262  opi2  4266  opth2  4273  opeqsn  4285  opeqpr  4286  uniop  4288  opelopaba  4300  braba  4301  opelopab  4306  brab  4307  opelopabaf  4308  unex  4476  snnex  4483  op1stb  4513  ifelpwun  4518  ifex  4521  onun2i  4527  onsucssi  4542  ontriexmidim  4558  ontr2exmid  4561  onsucsssucexmid  4563  onsucelsucexmid  4566  opthreg  4592  tfis  4619  finds  4636  finds2  4637  nnregexmid  4657  xpeq12i  4685  opelvv  4713  eqrelriiv  4757  eqrelrdv  4759  xpss  4771  xpex  4778  relop  4816  brco  4837  opelcnv  4848  brcnv  4849  asymref  5055  codir  5058  ssrnres  5112  dmprop  5144  dfco2  5169  cossxp  5192  cocnvss  5195  coex  5215  funsn  5306  fnsn  5312  feq23i  5402  resasplitss  5437  fabex  5446  fvex  5578  xpsn  5738  fmptap  5752  opabex  5786  acexmidlemv  5920  oveq12i  5934  oprabid  5954  oprabss  6008  caovcom  6081  opabex3  6179  iunex  6180  oprabex  6185  ofmres  6193  op1st  6204  op2nd  6205  fo1st  6215  fo2nd  6216  mpoex  6272  1stconst  6279  2ndconst  6280  algrflem  6287  dftpos4  6321  tpostpos  6322  tpossym  6334  frecex  6452  frecfnom  6459  sucinc  6503  fnoei  6510  oeiexg  6511  nnacli  6540  nnmcli  6541  elec  6633  ecovcom  6701  ecovass  6703  ecovdi  6705  fnmap  6714  mapval  6719  elmap  6736  elpm  6738  elpm2  6739  map0  6748  ixpconst  6767  entri  6845  endisj  6883  xpcomco  6885  phplem2  6914  ssfiexmid  6937  domfiexmid  6939  exmidpw2en  6973  unfiexmid  6979  unfiin  6987  inresflem  7126  casefun  7151  caserel  7153  caseinj  7155  omp1eomlem  7160  omp1eom  7161  endjusym  7162  djufun  7170  djuinj  7172  ctssdccl  7177  ctssdclemr  7178  nninfex  7187  infnninf  7190  fodjuomnilemdc  7210  ctssexmid  7216  exmidonfinlem  7260  dju1p1e2  7264  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  pw1dom2  7294  onntri35  7304  onntri45  7308  2oneel  7323  2omotaplemst  7325  1lt2pi  7407  indpi  7409  1nq  7433  rec1nq  7462  1lt2nq  7473  ltaddnq  7474  halfnqq  7477  prarloclemarch2  7486  prarloclemlt  7560  prarloclemcalc  7569  genpelxp  7578  ltexprlempr  7675  recexprlempr  7699  cauappcvgprlemcl  7720  cauappcvgprlemladd  7725  caucvgprlemcl  7743  caucvgprprlemcl  7771  suplocexprlemell  7780  suplocexprlemdisj  7787  suplocexprlemub  7790  0r  7817  1sr  7818  m1r  7819  m1p1sr  7827  m1m1sr  7828  0lt1sr  7832  1ne0sr  7833  1idsr  7835  recexgt0sr  7840  prsradd  7853  caucvgsrlemoffres  7867  caucvgsr  7869  mappsrprg  7871  map2psrprg  7872  pitonnlem1p1  7913  pitonnlem2  7914  pitoregt0  7916  peano2nnnn  7920  axi2m1  7942  axprecex  7947  axcnre  7948  nnindnn  7960  nntopi  7961  0cn  8018  addcli  8030  mulcli  8031  mulcomi  8032  readdcli  8039  remulcli  8040  rexpssxrxp  8071  ltrelxr  8087  gtneii  8122  lttri3i  8124  letri3i  8125  ltnsymi  8126  lenlti  8127  ltlei  8128  mulgt0i  8136  mulgt0ii  8137  0lt1  8153  addcomi  8170  pncan3oi  8242  resubcli  8289  subcli  8302  pncan3i  8303  negsubi  8304  subnegi  8305  subeq0i  8306  neg11i  8307  negcon1i  8308  negcon2i  8309  mulneg1i  8430  mulneg2i  8431  mul2negi  8432  addgt0ii  8518  ltnegi  8520  lenegi  8521  ltnegcon2i  8522  lesub0i  8523  ltaddposi  8524  posdifi  8525  ltnegcon1i  8526  lenegcon1i  8527  subge0i  8528  1ap0  8617  ltapii  8662  recrecapi  8771  dividapi  8772  div0api  8773  rec11apii  8788  divdiv32api  8794  recgt0ii  8934  ltrecii  8945  ltdiv23ii  8954  sup3exmid  8984  nnssre  8994  nnind  9006  nnmulcli  9012  nnsubi  9030  0le2  9080  1lt3  9162  2lt4  9164  1lt4  9165  3lt5  9167  2lt5  9168  1lt5  9169  4lt6  9171  3lt6  9172  2lt6  9173  1lt6  9174  5lt7  9176  4lt7  9177  3lt7  9178  2lt7  9179  1lt7  9180  6lt8  9182  5lt8  9183  4lt8  9184  3lt8  9185  2lt8  9186  1lt8  9187  7lt9  9189  6lt9  9190  5lt9  9191  4lt9  9192  3lt9  9193  2lt9  9194  1lt9  9195  2muline0  9216  nn0addcli  9286  nn0mulcli  9287  nn0addge1i  9297  nn0addge2i  9298  dfz2  9398  halfnz  9422  9p1e10  9459  numnncl  9466  numltc  9482  le9lt10  9483  nummac  9501  8lt10  9588  7lt10  9589  6lt10  9590  5lt10  9591  4lt10  9592  3lt10  9593  2lt10  9594  1lt10  9595  eluzaddi  9628  eluzsubi  9629  eluz2nn  9640  eluz4eluz2  9641  uzuzle23  9645  eluzge3nn  9646  divfnzn  9695  elq  9696  qreccl  9716  xrltnr  9854  mnfltpnf  9860  xaddmnf1  9923  pnfaddmnf  9925  mnfaddpnf  9926  xrex  9931  xaddid1  9937  xsubge0  9956  xposdif  9957  xleaddadd  9962  elicc2i  10014  ioomax  10023  iccmax  10024  ioopos  10025  elxrge0  10053  iccshftri  10070  iccshftli  10072  iccdili  10074  icccntri  10076  unitssre  10080  fz10  10121  fzpreddisj  10146  fz0to4untppr  10199  dfrp2  10353  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  frecfzennn  10518  xnn0nnen  10529  fnn0nninf  10530  fxnn0nninf  10531  0tonninf  10532  1tonninf  10533  m1expcl2  10653  m1expcl  10654  nn0expcli  10657  sqmuli  10714  cu2  10730  i3  10733  subsqi  10741  binom2subi  10747  bcpasc  10858  4bc2eq6  10866  hashinfom  10870  prhash2ex  10901  hashp1i  10902  rei  11064  imi  11065  readdi  11093  imaddi  11094  remuli  11095  immuli  11096  cjaddi  11097  cjmuli  11098  ipcni  11099  crrei  11101  crimi  11102  rexfiuz  11154  sqrt1  11211  sqrt4  11212  sqrt9  11213  abs1  11237  sqrtmulii  11299  abslti  11303  abslei  11304  abssubi  11315  absmuli  11316  sqabsaddi  11317  sqabssubi  11318  abstrii  11320  fimaxre2  11392  climz  11457  abscn2  11480  recn2  11482  imcn2  11483  climabs  11485  climre  11487  climim  11488  fsumcnv  11602  fsumrelem  11636  fsumre  11637  fsumim  11638  arisum2  11664  expcnv  11669  geo2sum2  11680  geo2lim  11681  0.999...  11686  geoihalfsum  11687  fprodcnv  11790  fprodge0  11802  fprodge1  11804  ege2le3  11836  ef0  11837  reeff1  11865  tan0  11896  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos1bnd  11924  cos2bnd  11925  sinltxirr  11926  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  sincos1sgn  11930  sincos2sgn  11931  cos12dec  11933  egt2lt3  11945  epos  11946  ene1  11950  eap1  11951  3dvds  12029  3dvdsdec  12030  3dvds2dec  12031  odd2np1lem  12037  n2dvds1  12077  z4even  12081  ndvdsi  12098  flodddiv4  12101  bitsp1o  12117  gcd0val  12127  6gcd4e2  12162  3lcm2e6woprm  12254  6lcm4e12  12255  3lcm2e6  12328  sqrt2irrlem  12329  phimullem  12393  pockthi  12527  4sqlem19  12578  dec2dvds  12580  dec5dvds2  12582  dec2nprm  12584  modxai  12585  gcdi  12589  gcdmodi  12590  numexpp1  12593  karatsuba  12599  2exp7  12603  xpnnen  12611  xpomen  12612  ennnfonelemj0  12618  ennnfonelem0  12622  ennnfonelemhf1o  12630  exmidunben  12643  qnnen  12648  unct  12659  setscom  12718  strleun  12782  prdsex  12940  imasival  12949  ismgm  13000  fn0g  13018  fngsum  13031  issgrp  13046  ismnddef  13059  isghm  13373  isrng  13490  rngmgpf  13493  isring  13556  mgpf  13567  dfrhm2  13710  rhmex  13713  isdomn  13825  rmodislmod  13907  lidlmex  14031  mopnset  14108  cnfldstr  14114  cnfldcj  14121  cnfld0  14127  cnfldplusf  14130  zringcrng  14148  zringmulr  14155  zringmpg  14162  znval  14192  psrval  14220  fnpsr  14221  txtopi  14497  txunii  14500  upxp  14508  uptx  14510  cnmpt1st  14524  cnmpt2nd  14525  txswaphmeolem  14556  qtopbasss  14757  cnmet  14766  cnfldms  14772  cnopncntop  14780  cnopn  14781  remet  14784  blssioo  14789  tgqioo  14791  tgioo2cntop  14793  tgioo2  14795  divcnap  14801  abscncf  14821  recncf  14822  imcncf  14823  cjcncf  14824  mulc1cncf  14825  cncfcn1cntop  14830  idcncf  14837  cdivcncfap  14840  expcncf  14845  cnrehmeocntop  14846  maxcncf  14851  mincncf  14852  ivthreinc  14881  hovercncf  14882  limccnp2lem  14912  limccnp2cntop  14913  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvrecap  14949  dveflem  14962  dvef  14963  sincn  15005  coscn  15006  reeff1oleme  15008  reeff1o  15009  cosz12  15016  sin0pilem1  15017  sin0pilem2  15018  pipos  15024  sinhalfpilem  15027  sincosq1lem  15061  sincosq1sgn  15062  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  cosq14gt0  15068  cosq23lt0  15069  coseq0q4123  15070  coseq00topi  15071  coseq0negpitopi  15072  tangtx  15074  sincos4thpi  15076  tan4thpi  15077  sincos6thpi  15078  pigt3  15080  cosordlem  15085  cosq34lt1  15086  cos02pilt1  15087  cos0pilt1  15088  ioocosf1o  15090  negpitopissre  15091  log1  15102  loge  15103  2logb9irr  15207  sqrt2cxp2logb9e3  15211  2logb9irrap  15213  mpodvdsmulf1o  15226  fsumdvdsmul  15227  1sgm2ppw  15231  lgsdir2lem2  15270  lgsdir2lem3  15271  lgseisenlem4  15314  2lgsoddprmlem3  15352  2sqlem9  15365  2sqlem10  15366  ex-fl  15371  ex-ceil  15372  ex-bc  15375  ex-dvds  15376  ex-gcd  15377  bj-charfunbi  15457  bj-unex  15565  bj-nn0suc0  15596  bj-nntrans  15597  bj-nnelirr  15599  012of  15640  2o01f  15641  pwle2  15643  nnsf  15649  peano3nninf  15651  exmidsbthrlem  15666  sbthom  15670  isomninnlem  15674  iooref1o  15678  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  apdiff  15692  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696  dceqnconst  15704  dcapnconst  15705  nconstwlpolemgt0  15708  taupi  15717