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  721  mp3an  1371  barbara  2176  eqeq12i  2243  el2v  2805  vtocl2  2856  spc2ev  2899  sbc2ie  3100  csbieb  3166  sseq12i  3252  uneq12i  3356  ineq12i  3403  ifssun  3617  nelpri  3690  ralpr  3721  rexpr  3722  preq12i  3748  dfop  3856  opeq12i  3862  breq12i  4092  mpteq2ia  4170  exmidundif  4290  exmidundifim  4291  opex  4315  opi2  4319  opth2  4326  opeqsn  4339  opeqpr  4340  uniop  4342  opelopaba  4354  braba  4355  opelopab  4360  brab  4361  opelopabaf  4362  unex  4532  snnex  4539  op1stb  4569  ifelpwun  4574  ifex  4577  onun2i  4583  onsucssi  4598  ontriexmidim  4614  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  opthreg  4648  tfis  4675  finds  4692  finds2  4693  nnregexmid  4713  xpeq12i  4741  opelvv  4769  eqrelriiv  4813  eqrelrdv  4815  xpss  4827  xpex  4834  relop  4872  brco  4893  opelcnv  4904  brcnv  4905  asymref  5114  codir  5117  ssrnres  5171  dmprop  5203  dfco2  5228  cossxp  5251  cocnvss  5254  coex  5274  funsn  5369  fnsn  5375  feq23i  5468  resasplitss  5507  fabex  5516  fvex  5649  xpsn  5813  fmptap  5833  opabex  5867  acexmidlemv  6005  oveq12i  6019  oprabid  6039  oprabss  6096  caovcom  6169  opabex3  6273  iunex  6274  oprabex  6279  ofmres  6287  op1st  6298  op2nd  6299  fo1st  6309  fo2nd  6310  mpoex  6366  1stconst  6373  2ndconst  6374  algrflem  6381  dftpos4  6415  tpostpos  6416  tpossym  6428  frecex  6546  frecfnom  6553  2oex  6585  sucinc  6599  fnoei  6606  oeiexg  6607  nnacli  6636  nnmcli  6637  elec  6729  ecovcom  6797  ecovass  6799  ecovdi  6801  fnmap  6810  mapval  6815  elmap  6832  elpm  6834  elpm2  6835  map0  6844  ixpconst  6863  entri  6946  endisj  6991  xpcomco  6993  phplem2  7022  1ndom2  7034  ssfiexmid  7046  domfiexmid  7048  exmidpw2en  7082  unfiexmid  7088  unfiin  7096  inresflem  7235  casefun  7260  caserel  7262  caseinj  7264  omp1eomlem  7269  omp1eom  7270  endjusym  7271  djufun  7279  djuinj  7281  ctssdccl  7286  ctssdclemr  7287  nninfex  7296  infnninf  7299  fodjuomnilemdc  7319  ctssexmid  7325  exmidonfinlem  7379  dju1p1e2  7383  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  exmidaclem  7398  pw1dom2  7420  onntri35  7430  onntri45  7434  2oneel  7450  2omotaplemst  7452  acnccim  7466  1lt2pi  7535  indpi  7537  1nq  7561  rec1nq  7590  1lt2nq  7601  ltaddnq  7602  halfnqq  7605  prarloclemarch2  7614  prarloclemlt  7688  prarloclemcalc  7697  genpelxp  7706  ltexprlempr  7803  recexprlempr  7827  cauappcvgprlemcl  7848  cauappcvgprlemladd  7853  caucvgprlemcl  7871  caucvgprprlemcl  7899  suplocexprlemell  7908  suplocexprlemdisj  7915  suplocexprlemub  7918  0r  7945  1sr  7946  m1r  7947  m1p1sr  7955  m1m1sr  7956  0lt1sr  7960  1ne0sr  7961  1idsr  7963  recexgt0sr  7968  prsradd  7981  caucvgsrlemoffres  7995  caucvgsr  7997  mappsrprg  7999  map2psrprg  8000  pitonnlem1p1  8041  pitonnlem2  8042  pitoregt0  8044  peano2nnnn  8048  axi2m1  8070  axprecex  8075  axcnre  8076  nnindnn  8088  nntopi  8089  0cn  8146  addcli  8158  mulcli  8159  mulcomi  8160  readdcli  8167  remulcli  8168  rexpssxrxp  8199  ltrelxr  8215  gtneii  8250  lttri3i  8252  letri3i  8253  ltnsymi  8254  lenlti  8255  ltlei  8256  mulgt0i  8264  mulgt0ii  8265  0lt1  8281  addcomi  8298  pncan3oi  8370  resubcli  8417  subcli  8430  pncan3i  8431  negsubi  8432  subnegi  8433  subeq0i  8434  neg11i  8435  negcon1i  8436  negcon2i  8437  mulneg1i  8558  mulneg2i  8559  mul2negi  8560  addgt0ii  8646  ltnegi  8648  lenegi  8649  ltnegcon2i  8650  lesub0i  8651  ltaddposi  8652  posdifi  8653  ltnegcon1i  8654  lenegcon1i  8655  subge0i  8656  1ap0  8745  ltapii  8790  recrecapi  8899  dividapi  8900  div0api  8901  rec11apii  8916  divdiv32api  8922  recgt0ii  9062  ltrecii  9073  ltdiv23ii  9082  sup3exmid  9112  nnssre  9122  nnind  9134  nnmulcli  9140  nnsubi  9158  0le2  9208  1lt3  9290  2lt4  9292  1lt4  9293  3lt5  9295  2lt5  9296  1lt5  9297  4lt6  9299  3lt6  9300  2lt6  9301  1lt6  9302  5lt7  9304  4lt7  9305  3lt7  9306  2lt7  9307  1lt7  9308  6lt8  9310  5lt8  9311  4lt8  9312  3lt8  9313  2lt8  9314  1lt8  9315  7lt9  9317  6lt9  9318  5lt9  9319  4lt9  9320  3lt9  9321  2lt9  9322  1lt9  9323  2muline0  9344  nn0addcli  9414  nn0mulcli  9415  nn0addge1i  9425  nn0addge2i  9426  dfz2  9527  halfnz  9551  9p1e10  9588  numnncl  9595  numltc  9611  le9lt10  9612  nummac  9630  8lt10  9717  7lt10  9718  6lt10  9719  5lt10  9720  4lt10  9721  3lt10  9722  2lt10  9723  1lt10  9724  eluzaddi  9757  eluzsubi  9758  eluz2nn  9769  eluz4eluz2  9770  uzuzle23  9774  eluzge3nn  9775  divfnzn  9824  elq  9825  qreccl  9845  xrltnr  9983  mnfltpnf  9989  xaddmnf1  10052  pnfaddmnf  10054  mnfaddpnf  10055  xrex  10060  xaddid1  10066  xsubge0  10085  xposdif  10086  xleaddadd  10091  elicc2i  10143  ioomax  10152  iccmax  10153  ioopos  10154  elxrge0  10182  iccshftri  10199  iccshftli  10201  iccdili  10203  icccntri  10205  unitssre  10209  fz10  10250  fzpreddisj  10275  fz0to4untppr  10328  dfrp2  10491  fldiv4p1lem1div2  10533  fldiv4lem1div2  10535  frecfzennn  10656  xnn0nnen  10667  fnn0nninf  10668  fxnn0nninf  10669  0tonninf  10670  1tonninf  10671  m1expcl2  10791  m1expcl  10792  nn0expcli  10795  sqmuli  10852  cu2  10868  i3  10871  subsqi  10879  binom2subi  10885  bcpasc  10996  4bc2eq6  11004  hashinfom  11008  prhash2ex  11039  hashp1i  11040  lsw0g  11128  swrdccat3blem  11279  rei  11418  imi  11419  readdi  11447  imaddi  11448  remuli  11449  immuli  11450  cjaddi  11451  cjmuli  11452  ipcni  11453  crrei  11455  crimi  11456  rexfiuz  11508  sqrt1  11565  sqrt4  11566  sqrt9  11567  abs1  11591  sqrtmulii  11653  abslti  11657  abslei  11658  abssubi  11669  absmuli  11670  sqabsaddi  11671  sqabssubi  11672  abstrii  11674  fimaxre2  11746  climz  11811  abscn2  11834  recn2  11836  imcn2  11837  climabs  11839  climre  11841  climim  11842  fsumcnv  11956  fsumrelem  11990  fsumre  11991  fsumim  11992  arisum2  12018  expcnv  12023  geo2sum2  12034  geo2lim  12035  0.999...  12040  geoihalfsum  12041  fprodcnv  12144  fprodge0  12156  fprodge1  12158  ege2le3  12190  ef0  12191  reeff1  12219  tan0  12250  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  cos1bnd  12278  cos2bnd  12279  sinltxirr  12280  sin01gt0  12281  cos01gt0  12282  sin02gt0  12283  sincos1sgn  12284  sincos2sgn  12285  cos12dec  12287  egt2lt3  12299  epos  12300  ene1  12304  eap1  12305  3dvds  12383  3dvdsdec  12384  3dvds2dec  12385  odd2np1lem  12391  n2dvds1  12431  z4even  12435  ndvdsi  12452  flodddiv4  12455  bitsp1o  12472  0bits  12478  gcd0val  12489  6gcd4e2  12524  3lcm2e6woprm  12616  6lcm4e12  12617  3lcm2e6  12690  sqrt2irrlem  12691  phimullem  12755  pockthi  12889  4sqlem19  12940  dec2dvds  12942  dec5dvds2  12944  dec2nprm  12946  modxai  12947  gcdi  12951  gcdmodi  12952  numexpp1  12955  karatsuba  12961  2exp7  12965  xpnnen  12973  xpomen  12974  ennnfonelemj0  12980  ennnfonelem0  12984  ennnfonelemhf1o  12992  exmidunben  13005  qnnen  13010  unct  13021  setscom  13080  strleun  13145  prdsex  13310  prdsvallem  13313  imasival  13347  ismgm  13398  fn0g  13416  fngsum  13429  issgrp  13444  ismnddef  13459  isghm  13788  isrng  13905  rngmgpf  13908  isring  13971  mgpf  13982  dfrhm2  14126  rhmex  14129  isdomn  14241  rmodislmod  14323  lidlmex  14447  mopnset  14524  cnfldstr  14530  cnfldcj  14537  cnfld0  14543  cnfldplusf  14546  zringcrng  14564  zringmulr  14571  zringmpg  14578  znval  14608  psrval  14638  fnpsr  14639  fnmpl  14665  txtopi  14943  txunii  14946  upxp  14954  uptx  14956  cnmpt1st  14970  cnmpt2nd  14971  txswaphmeolem  15002  qtopbasss  15203  cnmet  15212  cnfldms  15218  cnopncntop  15226  cnopn  15227  remet  15230  blssioo  15235  tgqioo  15237  tgioo2cntop  15239  tgioo2  15241  divcnap  15247  abscncf  15267  recncf  15268  imcncf  15269  cjcncf  15270  mulc1cncf  15271  cncfcn1cntop  15276  idcncf  15283  cdivcncfap  15286  expcncf  15291  cnrehmeocntop  15292  maxcncf  15297  mincncf  15298  ivthreinc  15327  hovercncf  15328  limccnp2lem  15358  limccnp2cntop  15359  dvcnp2cntop  15381  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvrecap  15395  dveflem  15408  dvef  15409  sincn  15451  coscn  15452  reeff1oleme  15454  reeff1o  15455  cosz12  15462  sin0pilem1  15463  sin0pilem2  15464  pipos  15470  sinhalfpilem  15473  sincosq1lem  15507  sincosq1sgn  15508  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  sinq12gt0  15512  cosq14gt0  15514  cosq23lt0  15515  coseq0q4123  15516  coseq00topi  15517  coseq0negpitopi  15518  tangtx  15520  sincos4thpi  15522  tan4thpi  15523  sincos6thpi  15524  pigt3  15526  cosordlem  15531  cosq34lt1  15532  cos02pilt1  15533  cos0pilt1  15534  ioocosf1o  15536  negpitopissre  15537  log1  15548  loge  15549  2logb9irr  15653  sqrt2cxp2logb9e3  15657  2logb9irrap  15659  mpodvdsmulf1o  15672  fsumdvdsmul  15673  1sgm2ppw  15677  lgsdir2lem2  15716  lgsdir2lem3  15717  lgseisenlem4  15760  2lgsoddprmlem3  15798  2sqlem9  15811  2sqlem10  15812  opvtxfvi  15836  opiedgfvi  15837  umgrbien  15918  upgr2wlkdc  16096  ex-fl  16113  ex-ceil  16114  ex-bc  16117  ex-dvds  16118  ex-gcd  16119  bj-charfunbi  16198  bj-unex  16306  bj-nn0suc0  16337  bj-nntrans  16338  bj-nnelirr  16340  012of  16386  2o01f  16387  pwle2  16393  nnsf  16401  peano3nninf  16403  exmidsbthrlem  16420  sbthom  16424  isomninnlem  16428  iooref1o  16432  trilpolemisumle  16436  trilpolemeq1  16438  trilpolemlt1  16439  apdiff  16446  iswomninnlem  16447  iswomni0  16449  ismkvnnlem  16450  dceqnconst  16458  dcapnconst  16459  nconstwlpolemgt0  16462  taupi  16471