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  3212  uneq12i  3316  ineq12i  3363  ifssun  3576  nelpri  3647  ralpr  3678  rexpr  3679  preq12i  3705  dfop  3808  opeq12i  3814  breq12i  4043  mpteq2ia  4120  exmidundif  4240  exmidundifim  4241  opex  4263  opi2  4267  opth2  4274  opeqsn  4286  opeqpr  4287  uniop  4289  opelopaba  4301  braba  4302  opelopab  4307  brab  4308  opelopabaf  4309  unex  4477  snnex  4484  op1stb  4514  ifelpwun  4519  ifex  4522  onun2i  4528  onsucssi  4543  ontriexmidim  4559  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmid  4567  opthreg  4593  tfis  4620  finds  4637  finds2  4638  nnregexmid  4658  xpeq12i  4686  opelvv  4714  eqrelriiv  4758  eqrelrdv  4760  xpss  4772  xpex  4779  relop  4817  brco  4838  opelcnv  4849  brcnv  4850  asymref  5056  codir  5059  ssrnres  5113  dmprop  5145  dfco2  5170  cossxp  5193  cocnvss  5196  coex  5216  funsn  5307  fnsn  5313  feq23i  5405  resasplitss  5440  fabex  5449  fvex  5581  xpsn  5741  fmptap  5755  opabex  5789  acexmidlemv  5923  oveq12i  5937  oprabid  5957  oprabss  6012  caovcom  6085  opabex3  6188  iunex  6189  oprabex  6194  ofmres  6202  op1st  6213  op2nd  6214  fo1st  6224  fo2nd  6225  mpoex  6281  1stconst  6288  2ndconst  6289  algrflem  6296  dftpos4  6330  tpostpos  6331  tpossym  6343  frecex  6461  frecfnom  6468  sucinc  6512  fnoei  6519  oeiexg  6520  nnacli  6549  nnmcli  6550  elec  6642  ecovcom  6710  ecovass  6712  ecovdi  6714  fnmap  6723  mapval  6728  elmap  6745  elpm  6747  elpm2  6748  map0  6757  ixpconst  6776  entri  6854  endisj  6892  xpcomco  6894  phplem2  6923  ssfiexmid  6946  domfiexmid  6948  exmidpw2en  6982  unfiexmid  6988  unfiin  6996  inresflem  7135  casefun  7160  caserel  7162  caseinj  7164  omp1eomlem  7169  omp1eom  7170  endjusym  7171  djufun  7179  djuinj  7181  ctssdccl  7186  ctssdclemr  7187  nninfex  7196  infnninf  7199  fodjuomnilemdc  7219  ctssexmid  7225  exmidonfinlem  7274  dju1p1e2  7278  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidaclem  7293  pw1dom2  7312  onntri35  7322  onntri45  7326  2oneel  7341  2omotaplemst  7343  acnccim  7357  1lt2pi  7426  indpi  7428  1nq  7452  rec1nq  7481  1lt2nq  7492  ltaddnq  7493  halfnqq  7496  prarloclemarch2  7505  prarloclemlt  7579  prarloclemcalc  7588  genpelxp  7597  ltexprlempr  7694  recexprlempr  7718  cauappcvgprlemcl  7739  cauappcvgprlemladd  7744  caucvgprlemcl  7762  caucvgprprlemcl  7790  suplocexprlemell  7799  suplocexprlemdisj  7806  suplocexprlemub  7809  0r  7836  1sr  7837  m1r  7838  m1p1sr  7846  m1m1sr  7847  0lt1sr  7851  1ne0sr  7852  1idsr  7854  recexgt0sr  7859  prsradd  7872  caucvgsrlemoffres  7886  caucvgsr  7888  mappsrprg  7890  map2psrprg  7891  pitonnlem1p1  7932  pitonnlem2  7933  pitoregt0  7935  peano2nnnn  7939  axi2m1  7961  axprecex  7966  axcnre  7967  nnindnn  7979  nntopi  7980  0cn  8037  addcli  8049  mulcli  8050  mulcomi  8051  readdcli  8058  remulcli  8059  rexpssxrxp  8090  ltrelxr  8106  gtneii  8141  lttri3i  8143  letri3i  8144  ltnsymi  8145  lenlti  8146  ltlei  8147  mulgt0i  8155  mulgt0ii  8156  0lt1  8172  addcomi  8189  pncan3oi  8261  resubcli  8308  subcli  8321  pncan3i  8322  negsubi  8323  subnegi  8324  subeq0i  8325  neg11i  8326  negcon1i  8327  negcon2i  8328  mulneg1i  8449  mulneg2i  8450  mul2negi  8451  addgt0ii  8537  ltnegi  8539  lenegi  8540  ltnegcon2i  8541  lesub0i  8542  ltaddposi  8543  posdifi  8544  ltnegcon1i  8545  lenegcon1i  8546  subge0i  8547  1ap0  8636  ltapii  8681  recrecapi  8790  dividapi  8791  div0api  8792  rec11apii  8807  divdiv32api  8813  recgt0ii  8953  ltrecii  8964  ltdiv23ii  8973  sup3exmid  9003  nnssre  9013  nnind  9025  nnmulcli  9031  nnsubi  9049  0le2  9099  1lt3  9181  2lt4  9183  1lt4  9184  3lt5  9186  2lt5  9187  1lt5  9188  4lt6  9190  3lt6  9191  2lt6  9192  1lt6  9193  5lt7  9195  4lt7  9196  3lt7  9197  2lt7  9198  1lt7  9199  6lt8  9201  5lt8  9202  4lt8  9203  3lt8  9204  2lt8  9205  1lt8  9206  7lt9  9208  6lt9  9209  5lt9  9210  4lt9  9211  3lt9  9212  2lt9  9213  1lt9  9214  2muline0  9235  nn0addcli  9305  nn0mulcli  9306  nn0addge1i  9316  nn0addge2i  9317  dfz2  9417  halfnz  9441  9p1e10  9478  numnncl  9485  numltc  9501  le9lt10  9502  nummac  9520  8lt10  9607  7lt10  9608  6lt10  9609  5lt10  9610  4lt10  9611  3lt10  9612  2lt10  9613  1lt10  9614  eluzaddi  9647  eluzsubi  9648  eluz2nn  9659  eluz4eluz2  9660  uzuzle23  9664  eluzge3nn  9665  divfnzn  9714  elq  9715  qreccl  9735  xrltnr  9873  mnfltpnf  9879  xaddmnf1  9942  pnfaddmnf  9944  mnfaddpnf  9945  xrex  9950  xaddid1  9956  xsubge0  9975  xposdif  9976  xleaddadd  9981  elicc2i  10033  ioomax  10042  iccmax  10043  ioopos  10044  elxrge0  10072  iccshftri  10089  iccshftli  10091  iccdili  10093  icccntri  10095  unitssre  10099  fz10  10140  fzpreddisj  10165  fz0to4untppr  10218  dfrp2  10372  fldiv4p1lem1div2  10414  fldiv4lem1div2  10416  frecfzennn  10537  xnn0nnen  10548  fnn0nninf  10549  fxnn0nninf  10550  0tonninf  10551  1tonninf  10552  m1expcl2  10672  m1expcl  10673  nn0expcli  10676  sqmuli  10733  cu2  10749  i3  10752  subsqi  10760  binom2subi  10766  bcpasc  10877  4bc2eq6  10885  hashinfom  10889  prhash2ex  10920  hashp1i  10921  rei  11083  imi  11084  readdi  11112  imaddi  11113  remuli  11114  immuli  11115  cjaddi  11116  cjmuli  11117  ipcni  11118  crrei  11120  crimi  11121  rexfiuz  11173  sqrt1  11230  sqrt4  11231  sqrt9  11232  abs1  11256  sqrtmulii  11318  abslti  11322  abslei  11323  abssubi  11334  absmuli  11335  sqabsaddi  11336  sqabssubi  11337  abstrii  11339  fimaxre2  11411  climz  11476  abscn2  11499  recn2  11501  imcn2  11502  climabs  11504  climre  11506  climim  11507  fsumcnv  11621  fsumrelem  11655  fsumre  11656  fsumim  11657  arisum2  11683  expcnv  11688  geo2sum2  11699  geo2lim  11700  0.999...  11705  geoihalfsum  11706  fprodcnv  11809  fprodge0  11821  fprodge1  11823  ege2le3  11855  ef0  11856  reeff1  11884  tan0  11915  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  cos1bnd  11943  cos2bnd  11944  sinltxirr  11945  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  sincos1sgn  11949  sincos2sgn  11950  cos12dec  11952  egt2lt3  11964  epos  11965  ene1  11969  eap1  11970  3dvds  12048  3dvdsdec  12049  3dvds2dec  12050  odd2np1lem  12056  n2dvds1  12096  z4even  12100  ndvdsi  12117  flodddiv4  12120  bitsp1o  12137  0bits  12143  gcd0val  12154  6gcd4e2  12189  3lcm2e6woprm  12281  6lcm4e12  12282  3lcm2e6  12355  sqrt2irrlem  12356  phimullem  12420  pockthi  12554  4sqlem19  12605  dec2dvds  12607  dec5dvds2  12609  dec2nprm  12611  modxai  12612  gcdi  12616  gcdmodi  12617  numexpp1  12620  karatsuba  12626  2exp7  12630  xpnnen  12638  xpomen  12639  ennnfonelemj0  12645  ennnfonelem0  12649  ennnfonelemhf1o  12657  exmidunben  12670  qnnen  12675  unct  12686  setscom  12745  strleun  12809  prdsex  12973  prdsvallem  12976  imasival  13010  ismgm  13061  fn0g  13079  fngsum  13092  issgrp  13107  ismnddef  13122  isghm  13451  isrng  13568  rngmgpf  13571  isring  13634  mgpf  13645  dfrhm2  13788  rhmex  13791  isdomn  13903  rmodislmod  13985  lidlmex  14109  mopnset  14186  cnfldstr  14192  cnfldcj  14199  cnfld0  14205  cnfldplusf  14208  zringcrng  14226  zringmulr  14233  zringmpg  14240  znval  14270  psrval  14298  fnpsr  14299  txtopi  14583  txunii  14586  upxp  14594  uptx  14596  cnmpt1st  14610  cnmpt2nd  14611  txswaphmeolem  14642  qtopbasss  14843  cnmet  14852  cnfldms  14858  cnopncntop  14866  cnopn  14867  remet  14870  blssioo  14875  tgqioo  14877  tgioo2cntop  14879  tgioo2  14881  divcnap  14887  abscncf  14907  recncf  14908  imcncf  14909  cjcncf  14910  mulc1cncf  14911  cncfcn1cntop  14916  idcncf  14923  cdivcncfap  14926  expcncf  14931  cnrehmeocntop  14932  maxcncf  14937  mincncf  14938  ivthreinc  14967  hovercncf  14968  limccnp2lem  14998  limccnp2cntop  14999  dvcnp2cntop  15021  dvaddxxbr  15023  dvmulxxbr  15024  dvcoapbr  15029  dvrecap  15035  dveflem  15048  dvef  15049  sincn  15091  coscn  15092  reeff1oleme  15094  reeff1o  15095  cosz12  15102  sin0pilem1  15103  sin0pilem2  15104  pipos  15110  sinhalfpilem  15113  sincosq1lem  15147  sincosq1sgn  15148  sincosq2sgn  15149  sincosq3sgn  15150  sincosq4sgn  15151  sinq12gt0  15152  cosq14gt0  15154  cosq23lt0  15155  coseq0q4123  15156  coseq00topi  15157  coseq0negpitopi  15158  tangtx  15160  sincos4thpi  15162  tan4thpi  15163  sincos6thpi  15164  pigt3  15166  cosordlem  15171  cosq34lt1  15172  cos02pilt1  15173  cos0pilt1  15174  ioocosf1o  15176  negpitopissre  15177  log1  15188  loge  15189  2logb9irr  15293  sqrt2cxp2logb9e3  15297  2logb9irrap  15299  mpodvdsmulf1o  15312  fsumdvdsmul  15313  1sgm2ppw  15317  lgsdir2lem2  15356  lgsdir2lem3  15357  lgseisenlem4  15400  2lgsoddprmlem3  15438  2sqlem9  15451  2sqlem10  15452  ex-fl  15457  ex-ceil  15458  ex-bc  15461  ex-dvds  15462  ex-gcd  15463  bj-charfunbi  15543  bj-unex  15651  bj-nn0suc0  15682  bj-nntrans  15683  bj-nnelirr  15685  012of  15726  2o01f  15727  pwle2  15731  nnsf  15738  peano3nninf  15740  exmidsbthrlem  15757  sbthom  15761  isomninnlem  15765  iooref1o  15769  trilpolemisumle  15773  trilpolemeq1  15775  trilpolemlt1  15776  apdiff  15783  iswomninnlem  15784  iswomni0  15786  ismkvnnlem  15787  dceqnconst  15795  dcapnconst  15796  nconstwlpolemgt0  15799  taupi  15808