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  718  mp3an  1350  barbara  2153  eqeq12i  2220  vtocl2  2829  spc2ev  2870  sbc2ie  3071  csbieb  3136  sseq12i  3222  uneq12i  3326  ineq12i  3373  ifssun  3586  nelpri  3658  ralpr  3689  rexpr  3690  preq12i  3716  dfop  3820  opeq12i  3826  breq12i  4056  mpteq2ia  4134  exmidundif  4254  exmidundifim  4255  opex  4277  opi2  4281  opth2  4288  opeqsn  4301  opeqpr  4302  uniop  4304  opelopaba  4316  braba  4317  opelopab  4322  brab  4323  opelopabaf  4324  unex  4492  snnex  4499  op1stb  4529  ifelpwun  4534  ifex  4537  onun2i  4543  onsucssi  4558  ontriexmidim  4574  ontr2exmid  4577  onsucsssucexmid  4579  onsucelsucexmid  4582  opthreg  4608  tfis  4635  finds  4652  finds2  4653  nnregexmid  4673  xpeq12i  4701  opelvv  4729  eqrelriiv  4773  eqrelrdv  4775  xpss  4787  xpex  4794  relop  4832  brco  4853  opelcnv  4864  brcnv  4865  asymref  5073  codir  5076  ssrnres  5130  dmprop  5162  dfco2  5187  cossxp  5210  cocnvss  5213  coex  5233  funsn  5327  fnsn  5333  feq23i  5426  resasplitss  5462  fabex  5471  fvex  5603  xpsn  5763  fmptap  5781  opabex  5815  acexmidlemv  5949  oveq12i  5963  oprabid  5983  oprabss  6038  caovcom  6111  opabex3  6214  iunex  6215  oprabex  6220  ofmres  6228  op1st  6239  op2nd  6240  fo1st  6250  fo2nd  6251  mpoex  6307  1stconst  6314  2ndconst  6315  algrflem  6322  dftpos4  6356  tpostpos  6357  tpossym  6369  frecex  6487  frecfnom  6494  sucinc  6538  fnoei  6545  oeiexg  6546  nnacli  6575  nnmcli  6576  elec  6668  ecovcom  6736  ecovass  6738  ecovdi  6740  fnmap  6749  mapval  6754  elmap  6771  elpm  6773  elpm2  6774  map0  6783  ixpconst  6802  entri  6885  endisj  6926  xpcomco  6928  phplem2  6957  ssfiexmid  6980  domfiexmid  6982  exmidpw2en  7016  unfiexmid  7022  unfiin  7030  inresflem  7169  casefun  7194  caserel  7196  caseinj  7198  omp1eomlem  7203  omp1eom  7204  endjusym  7205  djufun  7213  djuinj  7215  ctssdccl  7220  ctssdclemr  7221  nninfex  7230  infnninf  7233  fodjuomnilemdc  7253  ctssexmid  7259  exmidonfinlem  7308  dju1p1e2  7312  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  exmidaclem  7327  pw1dom2  7346  onntri35  7356  onntri45  7360  2oneel  7375  2omotaplemst  7377  acnccim  7391  1lt2pi  7460  indpi  7462  1nq  7486  rec1nq  7515  1lt2nq  7526  ltaddnq  7527  halfnqq  7530  prarloclemarch2  7539  prarloclemlt  7613  prarloclemcalc  7622  genpelxp  7631  ltexprlempr  7728  recexprlempr  7752  cauappcvgprlemcl  7773  cauappcvgprlemladd  7778  caucvgprlemcl  7796  caucvgprprlemcl  7824  suplocexprlemell  7833  suplocexprlemdisj  7840  suplocexprlemub  7843  0r  7870  1sr  7871  m1r  7872  m1p1sr  7880  m1m1sr  7881  0lt1sr  7885  1ne0sr  7886  1idsr  7888  recexgt0sr  7893  prsradd  7906  caucvgsrlemoffres  7920  caucvgsr  7922  mappsrprg  7924  map2psrprg  7925  pitonnlem1p1  7966  pitonnlem2  7967  pitoregt0  7969  peano2nnnn  7973  axi2m1  7995  axprecex  8000  axcnre  8001  nnindnn  8013  nntopi  8014  0cn  8071  addcli  8083  mulcli  8084  mulcomi  8085  readdcli  8092  remulcli  8093  rexpssxrxp  8124  ltrelxr  8140  gtneii  8175  lttri3i  8177  letri3i  8178  ltnsymi  8179  lenlti  8180  ltlei  8181  mulgt0i  8189  mulgt0ii  8190  0lt1  8206  addcomi  8223  pncan3oi  8295  resubcli  8342  subcli  8355  pncan3i  8356  negsubi  8357  subnegi  8358  subeq0i  8359  neg11i  8360  negcon1i  8361  negcon2i  8362  mulneg1i  8483  mulneg2i  8484  mul2negi  8485  addgt0ii  8571  ltnegi  8573  lenegi  8574  ltnegcon2i  8575  lesub0i  8576  ltaddposi  8577  posdifi  8578  ltnegcon1i  8579  lenegcon1i  8580  subge0i  8581  1ap0  8670  ltapii  8715  recrecapi  8824  dividapi  8825  div0api  8826  rec11apii  8841  divdiv32api  8847  recgt0ii  8987  ltrecii  8998  ltdiv23ii  9007  sup3exmid  9037  nnssre  9047  nnind  9059  nnmulcli  9065  nnsubi  9083  0le2  9133  1lt3  9215  2lt4  9217  1lt4  9218  3lt5  9220  2lt5  9221  1lt5  9222  4lt6  9224  3lt6  9225  2lt6  9226  1lt6  9227  5lt7  9229  4lt7  9230  3lt7  9231  2lt7  9232  1lt7  9233  6lt8  9235  5lt8  9236  4lt8  9237  3lt8  9238  2lt8  9239  1lt8  9240  7lt9  9242  6lt9  9243  5lt9  9244  4lt9  9245  3lt9  9246  2lt9  9247  1lt9  9248  2muline0  9269  nn0addcli  9339  nn0mulcli  9340  nn0addge1i  9350  nn0addge2i  9351  dfz2  9452  halfnz  9476  9p1e10  9513  numnncl  9520  numltc  9536  le9lt10  9537  nummac  9555  8lt10  9642  7lt10  9643  6lt10  9644  5lt10  9645  4lt10  9646  3lt10  9647  2lt10  9648  1lt10  9649  eluzaddi  9682  eluzsubi  9683  eluz2nn  9694  eluz4eluz2  9695  uzuzle23  9699  eluzge3nn  9700  divfnzn  9749  elq  9750  qreccl  9770  xrltnr  9908  mnfltpnf  9914  xaddmnf1  9977  pnfaddmnf  9979  mnfaddpnf  9980  xrex  9985  xaddid1  9991  xsubge0  10010  xposdif  10011  xleaddadd  10016  elicc2i  10068  ioomax  10077  iccmax  10078  ioopos  10079  elxrge0  10107  iccshftri  10124  iccshftli  10126  iccdili  10128  icccntri  10130  unitssre  10134  fz10  10175  fzpreddisj  10200  fz0to4untppr  10253  dfrp2  10413  fldiv4p1lem1div2  10455  fldiv4lem1div2  10457  frecfzennn  10578  xnn0nnen  10589  fnn0nninf  10590  fxnn0nninf  10591  0tonninf  10592  1tonninf  10593  m1expcl2  10713  m1expcl  10714  nn0expcli  10717  sqmuli  10774  cu2  10790  i3  10793  subsqi  10801  binom2subi  10807  bcpasc  10918  4bc2eq6  10926  hashinfom  10930  prhash2ex  10961  hashp1i  10962  lsw0g  11049  rei  11254  imi  11255  readdi  11283  imaddi  11284  remuli  11285  immuli  11286  cjaddi  11287  cjmuli  11288  ipcni  11289  crrei  11291  crimi  11292  rexfiuz  11344  sqrt1  11401  sqrt4  11402  sqrt9  11403  abs1  11427  sqrtmulii  11489  abslti  11493  abslei  11494  abssubi  11505  absmuli  11506  sqabsaddi  11507  sqabssubi  11508  abstrii  11510  fimaxre2  11582  climz  11647  abscn2  11670  recn2  11672  imcn2  11673  climabs  11675  climre  11677  climim  11678  fsumcnv  11792  fsumrelem  11826  fsumre  11827  fsumim  11828  arisum2  11854  expcnv  11859  geo2sum2  11870  geo2lim  11871  0.999...  11876  geoihalfsum  11877  fprodcnv  11980  fprodge0  11992  fprodge1  11994  ege2le3  12026  ef0  12027  reeff1  12055  tan0  12086  ef01bndlem  12111  sin01bnd  12112  cos01bnd  12113  cos1bnd  12114  cos2bnd  12115  sinltxirr  12116  sin01gt0  12117  cos01gt0  12118  sin02gt0  12119  sincos1sgn  12120  sincos2sgn  12121  cos12dec  12123  egt2lt3  12135  epos  12136  ene1  12140  eap1  12141  3dvds  12219  3dvdsdec  12220  3dvds2dec  12221  odd2np1lem  12227  n2dvds1  12267  z4even  12271  ndvdsi  12288  flodddiv4  12291  bitsp1o  12308  0bits  12314  gcd0val  12325  6gcd4e2  12360  3lcm2e6woprm  12452  6lcm4e12  12453  3lcm2e6  12526  sqrt2irrlem  12527  phimullem  12591  pockthi  12725  4sqlem19  12776  dec2dvds  12778  dec5dvds2  12780  dec2nprm  12782  modxai  12783  gcdi  12787  gcdmodi  12788  numexpp1  12791  karatsuba  12797  2exp7  12801  xpnnen  12809  xpomen  12810  ennnfonelemj0  12816  ennnfonelem0  12820  ennnfonelemhf1o  12828  exmidunben  12841  qnnen  12846  unct  12857  setscom  12916  strleun  12980  prdsex  13145  prdsvallem  13148  imasival  13182  ismgm  13233  fn0g  13251  fngsum  13264  issgrp  13279  ismnddef  13294  isghm  13623  isrng  13740  rngmgpf  13743  isring  13806  mgpf  13817  dfrhm2  13960  rhmex  13963  isdomn  14075  rmodislmod  14157  lidlmex  14281  mopnset  14358  cnfldstr  14364  cnfldcj  14371  cnfld0  14377  cnfldplusf  14380  zringcrng  14398  zringmulr  14405  zringmpg  14412  znval  14442  psrval  14472  fnpsr  14473  fnmpl  14499  txtopi  14777  txunii  14780  upxp  14788  uptx  14790  cnmpt1st  14804  cnmpt2nd  14805  txswaphmeolem  14836  qtopbasss  15037  cnmet  15046  cnfldms  15052  cnopncntop  15060  cnopn  15061  remet  15064  blssioo  15069  tgqioo  15071  tgioo2cntop  15073  tgioo2  15075  divcnap  15081  abscncf  15101  recncf  15102  imcncf  15103  cjcncf  15104  mulc1cncf  15105  cncfcn1cntop  15110  idcncf  15117  cdivcncfap  15120  expcncf  15125  cnrehmeocntop  15126  maxcncf  15131  mincncf  15132  ivthreinc  15161  hovercncf  15162  limccnp2lem  15192  limccnp2cntop  15193  dvcnp2cntop  15215  dvaddxxbr  15217  dvmulxxbr  15218  dvcoapbr  15223  dvrecap  15229  dveflem  15242  dvef  15243  sincn  15285  coscn  15286  reeff1oleme  15288  reeff1o  15289  cosz12  15296  sin0pilem1  15297  sin0pilem2  15298  pipos  15304  sinhalfpilem  15307  sincosq1lem  15341  sincosq1sgn  15342  sincosq2sgn  15343  sincosq3sgn  15344  sincosq4sgn  15345  sinq12gt0  15346  cosq14gt0  15348  cosq23lt0  15349  coseq0q4123  15350  coseq00topi  15351  coseq0negpitopi  15352  tangtx  15354  sincos4thpi  15356  tan4thpi  15357  sincos6thpi  15358  pigt3  15360  cosordlem  15365  cosq34lt1  15366  cos02pilt1  15367  cos0pilt1  15368  ioocosf1o  15370  negpitopissre  15371  log1  15382  loge  15383  2logb9irr  15487  sqrt2cxp2logb9e3  15491  2logb9irrap  15493  mpodvdsmulf1o  15506  fsumdvdsmul  15507  1sgm2ppw  15511  lgsdir2lem2  15550  lgsdir2lem3  15551  lgseisenlem4  15594  2lgsoddprmlem3  15632  2sqlem9  15645  2sqlem10  15646  opvtxfvi  15670  opiedgfvi  15671  ex-fl  15735  ex-ceil  15736  ex-bc  15739  ex-dvds  15740  ex-gcd  15741  bj-charfunbi  15821  bj-unex  15929  bj-nn0suc0  15960  bj-nntrans  15961  bj-nnelirr  15963  012of  16004  2o01f  16005  pwle2  16009  nnsf  16016  peano3nninf  16018  exmidsbthrlem  16035  sbthom  16039  isomninnlem  16043  iooref1o  16047  trilpolemisumle  16051  trilpolemeq1  16053  trilpolemlt1  16054  apdiff  16061  iswomninnlem  16062  iswomni0  16064  ismkvnnlem  16065  dceqnconst  16073  dcapnconst  16074  nconstwlpolemgt0  16077  taupi  16086