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  723  mp3an  1373  barbara  2178  eqeq12i  2245  el2v  2808  vtocl2  2859  spc2ev  2902  sbc2ie  3103  csbieb  3169  sseq12i  3255  uneq12i  3359  ineq12i  3406  ifssun  3620  nelpri  3693  ralpr  3724  rexpr  3725  preq12i  3753  dfop  3861  opeq12i  3867  breq12i  4097  mpteq2ia  4175  exmidundif  4296  exmidundifim  4297  opex  4321  opi2  4325  opth2  4332  opeqsn  4345  opeqpr  4346  uniop  4348  opelopaba  4360  braba  4361  opelopab  4366  brab  4367  opelopabaf  4368  unex  4538  snnex  4545  op1stb  4575  ifelpwun  4580  ifex  4583  onun2i  4589  onsucssi  4604  ontriexmidim  4620  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  opthreg  4654  tfis  4681  finds  4698  finds2  4699  nnregexmid  4719  xpeq12i  4747  opelvv  4776  eqrelriiv  4820  eqrelrdv  4822  xpss  4834  xpex  4842  relop  4880  brco  4901  opelcnv  4912  brcnv  4913  asymref  5122  codir  5125  ssrnres  5179  dmprop  5211  dfco2  5236  cossxp  5259  cocnvss  5262  coex  5282  funsn  5378  fnsn  5384  feq23i  5477  resasplitss  5516  fabex  5525  fvex  5659  xpsn  5824  fmptap  5844  opabex  5878  acexmidlemv  6016  oveq12i  6030  oprabid  6050  oprabss  6107  caovcom  6180  opabex3  6284  iunex  6285  oprabex  6290  ofmres  6298  op1st  6309  op2nd  6310  fo1st  6320  fo2nd  6321  mpoex  6379  1stconst  6386  2ndconst  6387  algrflem  6394  dftpos4  6429  tpostpos  6430  tpossym  6442  frecex  6560  frecfnom  6567  2oex  6599  sucinc  6613  fnoei  6620  oeiexg  6621  nnacli  6650  nnmcli  6651  elec  6743  ecovcom  6811  ecovass  6813  ecovdi  6815  fnmap  6824  mapval  6829  elmap  6846  elpm  6848  elpm2  6849  map0  6858  ixpconst  6877  entri  6960  endisj  7008  xpcomco  7010  phplem2  7039  1ndom2  7051  ssfiexmid  7063  domfiexmid  7067  exmidpw2en  7104  unfiexmid  7110  unfiin  7118  inresflem  7259  casefun  7284  caserel  7286  caseinj  7288  omp1eomlem  7293  omp1eom  7294  endjusym  7295  djufun  7303  djuinj  7305  ctssdccl  7310  ctssdclemr  7311  nninfex  7320  infnninf  7323  fodjuomnilemdc  7343  ctssexmid  7349  exmidonfinlem  7404  dju1p1e2  7408  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  pw1dom2  7445  onntri35  7455  onntri45  7459  2oneel  7475  2omotaplemst  7477  acnccim  7491  1lt2pi  7560  indpi  7562  1nq  7586  rec1nq  7615  1lt2nq  7626  ltaddnq  7627  halfnqq  7630  prarloclemarch2  7639  prarloclemlt  7713  prarloclemcalc  7722  genpelxp  7731  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  cauappcvgprlemladd  7878  caucvgprlemcl  7896  caucvgprprlemcl  7924  suplocexprlemell  7933  suplocexprlemdisj  7940  suplocexprlemub  7943  0r  7970  1sr  7971  m1r  7972  m1p1sr  7980  m1m1sr  7981  0lt1sr  7985  1ne0sr  7986  1idsr  7988  recexgt0sr  7993  prsradd  8006  caucvgsrlemoffres  8020  caucvgsr  8022  mappsrprg  8024  map2psrprg  8025  pitonnlem1p1  8066  pitonnlem2  8067  pitoregt0  8069  peano2nnnn  8073  axi2m1  8095  axprecex  8100  axcnre  8101  nnindnn  8113  nntopi  8114  0cn  8171  addcli  8183  mulcli  8184  mulcomi  8185  readdcli  8192  remulcli  8193  rexpssxrxp  8224  ltrelxr  8240  gtneii  8275  lttri3i  8277  letri3i  8278  ltnsymi  8279  lenlti  8280  ltlei  8281  mulgt0i  8289  mulgt0ii  8290  0lt1  8306  addcomi  8323  pncan3oi  8395  resubcli  8442  subcli  8455  pncan3i  8456  negsubi  8457  subnegi  8458  subeq0i  8459  neg11i  8460  negcon1i  8461  negcon2i  8462  mulneg1i  8583  mulneg2i  8584  mul2negi  8585  addgt0ii  8671  ltnegi  8673  lenegi  8674  ltnegcon2i  8675  lesub0i  8676  ltaddposi  8677  posdifi  8678  ltnegcon1i  8679  lenegcon1i  8680  subge0i  8681  1ap0  8770  ltapii  8815  recrecapi  8924  dividapi  8925  div0api  8926  rec11apii  8941  divdiv32api  8947  recgt0ii  9087  ltrecii  9098  ltdiv23ii  9107  sup3exmid  9137  nnssre  9147  nnind  9159  nnmulcli  9165  nnsubi  9183  0le2  9233  1lt3  9315  2lt4  9317  1lt4  9318  3lt5  9320  2lt5  9321  1lt5  9322  4lt6  9324  3lt6  9325  2lt6  9326  1lt6  9327  5lt7  9329  4lt7  9330  3lt7  9331  2lt7  9332  1lt7  9333  6lt8  9335  5lt8  9336  4lt8  9337  3lt8  9338  2lt8  9339  1lt8  9340  7lt9  9342  6lt9  9343  5lt9  9344  4lt9  9345  3lt9  9346  2lt9  9347  1lt9  9348  2muline0  9369  nn0addcli  9439  nn0mulcli  9440  nn0addge1i  9450  nn0addge2i  9451  dfz2  9552  halfnz  9576  9p1e10  9613  numnncl  9620  numltc  9636  le9lt10  9637  nummac  9655  8lt10  9742  7lt10  9743  6lt10  9744  5lt10  9745  4lt10  9746  3lt10  9747  2lt10  9748  1lt10  9749  eluzaddi  9783  eluzsubi  9784  uzuzle23  9796  uzuzle24  9797  uzuzle34  9798  eluz2nn  9800  eluz4eluz2  9802  eluzge3nn  9806  divfnzn  9855  elq  9856  qreccl  9876  xrltnr  10014  mnfltpnf  10020  xaddmnf1  10083  pnfaddmnf  10085  mnfaddpnf  10086  xrex  10091  xaddid1  10097  xsubge0  10116  xposdif  10117  xleaddadd  10122  elicc2i  10174  ioomax  10183  iccmax  10184  ioopos  10185  elxrge0  10213  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  unitssre  10240  fz10  10281  fzpreddisj  10306  fz0to4untppr  10359  dfrp2  10524  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  frecfzennn  10689  xnn0nnen  10700  fnn0nninf  10701  fxnn0nninf  10702  0tonninf  10703  1tonninf  10704  m1expcl2  10824  m1expcl  10825  nn0expcli  10828  sqmuli  10885  cu2  10901  i3  10904  subsqi  10912  binom2subi  10918  bcpasc  11029  4bc2eq6  11037  hashinfom  11041  prhash2ex  11074  hashp1i  11075  lsw0g  11163  swrdccat3blem  11321  rei  11461  imi  11462  readdi  11490  imaddi  11491  remuli  11492  immuli  11493  cjaddi  11494  cjmuli  11495  ipcni  11496  crrei  11498  crimi  11499  rexfiuz  11551  sqrt1  11608  sqrt4  11609  sqrt9  11610  abs1  11634  sqrtmulii  11696  abslti  11700  abslei  11701  abssubi  11712  absmuli  11713  sqabsaddi  11714  sqabssubi  11715  abstrii  11717  fimaxre2  11789  climz  11854  abscn2  11877  recn2  11879  imcn2  11880  climabs  11882  climre  11884  climim  11885  fsumcnv  12000  fsumrelem  12034  fsumre  12035  fsumim  12036  arisum2  12062  expcnv  12067  geo2sum2  12078  geo2lim  12079  0.999...  12084  geoihalfsum  12085  fprodcnv  12188  fprodge0  12200  fprodge1  12202  ege2le3  12234  ef0  12235  reeff1  12263  tan0  12294  ef01bndlem  12319  sin01bnd  12320  cos01bnd  12321  cos1bnd  12322  cos2bnd  12323  sinltxirr  12324  sin01gt0  12325  cos01gt0  12326  sin02gt0  12327  sincos1sgn  12328  sincos2sgn  12329  cos12dec  12331  egt2lt3  12343  epos  12344  ene1  12348  eap1  12349  3dvds  12427  3dvdsdec  12428  3dvds2dec  12429  odd2np1lem  12435  n2dvds1  12475  z4even  12479  ndvdsi  12496  flodddiv4  12499  bitsp1o  12516  0bits  12522  gcd0val  12533  6gcd4e2  12568  3lcm2e6woprm  12660  6lcm4e12  12661  3lcm2e6  12734  sqrt2irrlem  12735  phimullem  12799  pockthi  12933  4sqlem19  12984  dec2dvds  12986  dec5dvds2  12988  dec2nprm  12990  modxai  12991  gcdi  12995  gcdmodi  12996  numexpp1  12999  karatsuba  13005  2exp7  13009  xpnnen  13017  xpomen  13018  ennnfonelemj0  13024  ennnfonelem0  13028  ennnfonelemhf1o  13036  exmidunben  13049  qnnen  13054  unct  13065  setscom  13124  strleun  13189  prdsex  13354  prdsvallem  13357  imasival  13391  ismgm  13442  fn0g  13460  fngsum  13473  issgrp  13488  ismnddef  13503  isghm  13832  isrng  13950  rngmgpf  13953  isring  14016  mgpf  14027  dfrhm2  14171  rhmex  14174  isdomn  14286  rmodislmod  14368  lidlmex  14492  mopnset  14569  cnfldstr  14575  cnfldcj  14582  cnfld0  14588  cnfldplusf  14591  zringcrng  14609  zringmulr  14616  zringmpg  14623  znval  14653  psrval  14683  fnpsr  14684  fnmpl  14710  txtopi  14988  txunii  14991  upxp  14999  uptx  15001  cnmpt1st  15015  cnmpt2nd  15016  txswaphmeolem  15047  qtopbasss  15248  cnmet  15257  cnfldms  15263  cnopncntop  15271  cnopn  15272  remet  15275  blssioo  15280  tgqioo  15282  tgioo2cntop  15284  tgioo2  15286  divcnap  15292  abscncf  15312  recncf  15313  imcncf  15314  cjcncf  15315  mulc1cncf  15316  cncfcn1cntop  15321  idcncf  15328  cdivcncfap  15331  expcncf  15336  cnrehmeocntop  15337  maxcncf  15342  mincncf  15343  ivthreinc  15372  hovercncf  15373  limccnp2lem  15403  limccnp2cntop  15404  dvcnp2cntop  15426  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  dvrecap  15440  dveflem  15453  dvef  15454  sincn  15496  coscn  15497  reeff1oleme  15499  reeff1o  15500  cosz12  15507  sin0pilem1  15508  sin0pilem2  15509  pipos  15515  sinhalfpilem  15518  sincosq1lem  15552  sincosq1sgn  15553  sincosq2sgn  15554  sincosq3sgn  15555  sincosq4sgn  15556  sinq12gt0  15557  cosq14gt0  15559  cosq23lt0  15560  coseq0q4123  15561  coseq00topi  15562  coseq0negpitopi  15563  tangtx  15565  sincos4thpi  15567  tan4thpi  15568  sincos6thpi  15569  pigt3  15571  cosordlem  15576  cosq34lt1  15577  cos02pilt1  15578  cos0pilt1  15579  ioocosf1o  15581  negpitopissre  15582  log1  15593  loge  15594  2logb9irr  15698  sqrt2cxp2logb9e3  15702  2logb9irrap  15704  mpodvdsmulf1o  15717  fsumdvdsmul  15718  1sgm2ppw  15722  lgsdir2lem2  15761  lgsdir2lem3  15762  lgseisenlem4  15805  2lgsoddprmlem3  15843  2sqlem9  15856  2sqlem10  15857  opvtxfvi  15881  opiedgfvi  15882  umgrbien  15964  usgrprc  16106  vtxdfifiun  16151  upgr2wlkdc  16231  ex-fl  16338  ex-ceil  16339  ex-bc  16342  ex-dvds  16343  ex-gcd  16344  bj-charfunbi  16427  bj-unex  16535  bj-nn0suc0  16566  bj-nntrans  16567  bj-nnelirr  16569  012of  16613  2o01f  16614  pwle2  16620  nnsf  16628  peano3nninf  16630  exmidsbthrlem  16647  sbthom  16651  isomninnlem  16655  iooref1o  16659  trilpolemisumle  16663  trilpolemeq1  16665  trilpolemlt1  16666  apdiff  16673  iswomninnlem  16674  iswomni0  16676  ismkvnnlem  16677  dceqnconst  16685  dcapnconst  16686  nconstwlpolemgt0  16689  taupi  16698