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  2140  eqeq12i  2207  vtocl2  2815  spc2ev  2856  sbc2ie  3057  csbieb  3122  sseq12i  3207  uneq12i  3311  ineq12i  3358  ifssun  3571  nelpri  3642  ralpr  3673  rexpr  3674  preq12i  3700  dfop  3803  opeq12i  3809  breq12i  4038  mpteq2ia  4115  exmidundif  4235  exmidundifim  4236  opex  4258  opi2  4262  opth2  4269  opeqsn  4281  opeqpr  4282  uniop  4284  opelopaba  4296  braba  4297  opelopab  4302  brab  4303  opelopabaf  4304  unex  4472  snnex  4479  op1stb  4509  ifelpwun  4514  ifex  4517  onun2i  4523  onsucssi  4538  ontriexmidim  4554  ontr2exmid  4557  onsucsssucexmid  4559  onsucelsucexmid  4562  opthreg  4588  tfis  4615  finds  4632  finds2  4633  nnregexmid  4653  xpeq12i  4681  opelvv  4709  eqrelriiv  4753  eqrelrdv  4755  xpss  4767  xpex  4774  relop  4812  brco  4833  opelcnv  4844  brcnv  4845  asymref  5051  codir  5054  ssrnres  5108  dmprop  5140  dfco2  5165  cossxp  5188  cocnvss  5191  coex  5211  funsn  5302  fnsn  5308  feq23i  5398  resasplitss  5433  fabex  5442  fvex  5574  xpsn  5734  fmptap  5748  opabex  5782  acexmidlemv  5916  oveq12i  5930  oprabid  5950  oprabss  6004  caovcom  6076  opabex3  6174  iunex  6175  oprabex  6180  ofmres  6188  op1st  6199  op2nd  6200  fo1st  6210  fo2nd  6211  mpoex  6267  1stconst  6274  2ndconst  6275  algrflem  6282  dftpos4  6316  tpostpos  6317  tpossym  6329  frecex  6447  frecfnom  6454  sucinc  6498  fnoei  6505  oeiexg  6506  nnacli  6535  nnmcli  6536  elec  6628  ecovcom  6696  ecovass  6698  ecovdi  6700  fnmap  6709  mapval  6714  elmap  6731  elpm  6733  elpm2  6734  map0  6743  ixpconst  6762  entri  6840  endisj  6878  xpcomco  6880  phplem2  6909  ssfiexmid  6932  domfiexmid  6934  exmidpw2en  6968  unfiexmid  6974  unfiin  6982  inresflem  7119  casefun  7144  caserel  7146  caseinj  7148  omp1eomlem  7153  omp1eom  7154  endjusym  7155  djufun  7163  djuinj  7165  ctssdccl  7170  ctssdclemr  7171  nninfex  7180  infnninf  7183  fodjuomnilemdc  7203  ctssexmid  7209  exmidonfinlem  7253  dju1p1e2  7257  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  pw1dom2  7287  onntri35  7297  onntri45  7301  2oneel  7316  2omotaplemst  7318  1lt2pi  7400  indpi  7402  1nq  7426  rec1nq  7455  1lt2nq  7466  ltaddnq  7467  halfnqq  7470  prarloclemarch2  7479  prarloclemlt  7553  prarloclemcalc  7562  genpelxp  7571  ltexprlempr  7668  recexprlempr  7692  cauappcvgprlemcl  7713  cauappcvgprlemladd  7718  caucvgprlemcl  7736  caucvgprprlemcl  7764  suplocexprlemell  7773  suplocexprlemdisj  7780  suplocexprlemub  7783  0r  7810  1sr  7811  m1r  7812  m1p1sr  7820  m1m1sr  7821  0lt1sr  7825  1ne0sr  7826  1idsr  7828  recexgt0sr  7833  prsradd  7846  caucvgsrlemoffres  7860  caucvgsr  7862  mappsrprg  7864  map2psrprg  7865  pitonnlem1p1  7906  pitonnlem2  7907  pitoregt0  7909  peano2nnnn  7913  axi2m1  7935  axprecex  7940  axcnre  7941  nnindnn  7953  nntopi  7954  0cn  8011  addcli  8023  mulcli  8024  mulcomi  8025  readdcli  8032  remulcli  8033  rexpssxrxp  8064  ltrelxr  8080  gtneii  8115  lttri3i  8117  letri3i  8118  ltnsymi  8119  lenlti  8120  ltlei  8121  mulgt0i  8129  mulgt0ii  8130  0lt1  8146  addcomi  8163  pncan3oi  8235  resubcli  8282  subcli  8295  pncan3i  8296  negsubi  8297  subnegi  8298  subeq0i  8299  neg11i  8300  negcon1i  8301  negcon2i  8302  mulneg1i  8423  mulneg2i  8424  mul2negi  8425  addgt0ii  8510  ltnegi  8512  lenegi  8513  ltnegcon2i  8514  lesub0i  8515  ltaddposi  8516  posdifi  8517  ltnegcon1i  8518  lenegcon1i  8519  subge0i  8520  1ap0  8609  ltapii  8654  recrecapi  8763  dividapi  8764  div0api  8765  rec11apii  8780  divdiv32api  8786  recgt0ii  8926  ltrecii  8937  ltdiv23ii  8946  sup3exmid  8976  nnssre  8986  nnind  8998  nnmulcli  9004  nnsubi  9022  0le2  9072  1lt3  9153  2lt4  9155  1lt4  9156  3lt5  9158  2lt5  9159  1lt5  9160  4lt6  9162  3lt6  9163  2lt6  9164  1lt6  9165  5lt7  9167  4lt7  9168  3lt7  9169  2lt7  9170  1lt7  9171  6lt8  9173  5lt8  9174  4lt8  9175  3lt8  9176  2lt8  9177  1lt8  9178  7lt9  9180  6lt9  9181  5lt9  9182  4lt9  9183  3lt9  9184  2lt9  9185  1lt9  9186  2muline0  9207  nn0addcli  9277  nn0mulcli  9278  nn0addge1i  9288  nn0addge2i  9289  dfz2  9389  halfnz  9413  9p1e10  9450  numnncl  9457  numltc  9473  le9lt10  9474  nummac  9492  8lt10  9579  7lt10  9580  6lt10  9581  5lt10  9582  4lt10  9583  3lt10  9584  2lt10  9585  1lt10  9586  eluzaddi  9619  eluzsubi  9620  eluz2nn  9631  eluz4eluz2  9632  uzuzle23  9636  eluzge3nn  9637  divfnzn  9686  elq  9687  qreccl  9707  xrltnr  9845  mnfltpnf  9851  xaddmnf1  9914  pnfaddmnf  9916  mnfaddpnf  9917  xrex  9922  xaddid1  9928  xsubge0  9947  xposdif  9948  xleaddadd  9953  elicc2i  10005  ioomax  10014  iccmax  10015  ioopos  10016  elxrge0  10044  iccshftri  10061  iccshftli  10063  iccdili  10065  icccntri  10067  unitssre  10071  fz10  10112  fzpreddisj  10137  fz0to4untppr  10190  dfrp2  10332  fldiv4p1lem1div2  10374  fldiv4lem1div2  10376  frecfzennn  10497  xnn0nnen  10508  fnn0nninf  10509  fxnn0nninf  10510  0tonninf  10511  1tonninf  10512  m1expcl2  10632  m1expcl  10633  nn0expcli  10636  sqmuli  10693  cu2  10709  i3  10712  subsqi  10720  binom2subi  10726  bcpasc  10837  4bc2eq6  10845  hashinfom  10849  prhash2ex  10880  hashp1i  10881  rei  11043  imi  11044  readdi  11072  imaddi  11073  remuli  11074  immuli  11075  cjaddi  11076  cjmuli  11077  ipcni  11078  crrei  11080  crimi  11081  rexfiuz  11133  sqrt1  11190  sqrt4  11191  sqrt9  11192  abs1  11216  sqrtmulii  11278  abslti  11282  abslei  11283  abssubi  11294  absmuli  11295  sqabsaddi  11296  sqabssubi  11297  abstrii  11299  fimaxre2  11370  climz  11435  abscn2  11458  recn2  11460  imcn2  11461  climabs  11463  climre  11465  climim  11466  fsumcnv  11580  fsumrelem  11614  fsumre  11615  fsumim  11616  arisum2  11642  expcnv  11647  geo2sum2  11658  geo2lim  11659  0.999...  11664  geoihalfsum  11665  fprodcnv  11768  fprodge0  11780  fprodge1  11782  ege2le3  11814  ef0  11815  reeff1  11843  tan0  11874  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  cos1bnd  11902  cos2bnd  11903  sinltxirr  11904  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  sincos1sgn  11908  sincos2sgn  11909  cos12dec  11911  egt2lt3  11923  epos  11924  ene1  11928  eap1  11929  3dvdsdec  12006  3dvds2dec  12007  odd2np1lem  12013  n2dvds1  12053  z4even  12057  ndvdsi  12074  flodddiv4  12075  gcd0val  12097  6gcd4e2  12132  3lcm2e6woprm  12224  6lcm4e12  12225  3lcm2e6  12298  sqrt2irrlem  12299  phimullem  12363  pockthi  12496  4sqlem19  12547  xpnnen  12551  xpomen  12552  ennnfonelemj0  12558  ennnfonelem0  12562  ennnfonelemhf1o  12570  exmidunben  12583  qnnen  12588  unct  12599  setscom  12658  strleun  12722  prdsex  12880  imasival  12889  ismgm  12940  fn0g  12958  fngsum  12971  issgrp  12986  ismnddef  12999  isghm  13313  isrng  13430  rngmgpf  13433  isring  13496  mgpf  13507  dfrhm2  13650  rhmex  13653  isdomn  13765  rmodislmod  13847  lidlmex  13971  cnfldstr  14049  cnfldcj  14056  cnfld0  14059  cnfldplusf  14062  zringcrng  14080  zringmulr  14087  zringmpg  14094  znval  14124  psrval  14152  fnpsr  14153  txtopi  14429  txunii  14432  upxp  14440  uptx  14442  cnmpt1st  14456  cnmpt2nd  14457  txswaphmeolem  14488  qtopbasss  14689  cnmet  14698  cnopncntop  14705  remet  14708  blssioo  14713  tgqioo  14715  tgioo2cntop  14717  divcnap  14723  abscncf  14740  recncf  14741  imcncf  14742  cjcncf  14743  mulc1cncf  14744  cncfcn1cntop  14749  idcncf  14755  cdivcncfap  14758  expcncf  14763  cnrehmeocntop  14764  maxcncf  14769  mincncf  14770  ivthreinc  14799  hovercncf  14800  limccnp2lem  14830  limccnp2cntop  14831  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvrecap  14862  dveflem  14872  dvef  14873  sincn  14904  coscn  14905  reeff1oleme  14907  reeff1o  14908  cosz12  14915  sin0pilem1  14916  sin0pilem2  14917  pipos  14923  sinhalfpilem  14926  sincosq1lem  14960  sincosq1sgn  14961  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  cosq14gt0  14967  cosq23lt0  14968  coseq0q4123  14969  coseq00topi  14970  coseq0negpitopi  14971  tangtx  14973  sincos4thpi  14975  tan4thpi  14976  sincos6thpi  14977  pigt3  14979  cosordlem  14984  cosq34lt1  14985  cos02pilt1  14986  cos0pilt1  14987  ioocosf1o  14989  negpitopissre  14990  log1  15001  loge  15002  2logb9irr  15103  sqrt2cxp2logb9e3  15107  2logb9irrap  15109  lgsdir2lem2  15145  lgsdir2lem3  15146  lgseisenlem4  15189  2lgsoddprmlem3  15199  2sqlem9  15211  2sqlem10  15212  ex-fl  15217  ex-ceil  15218  ex-bc  15221  ex-dvds  15222  ex-gcd  15223  bj-charfunbi  15303  bj-unex  15411  bj-nn0suc0  15442  bj-nntrans  15443  bj-nnelirr  15445  012of  15486  2o01f  15487  pwle2  15489  nnsf  15495  peano3nninf  15497  exmidsbthrlem  15512  sbthom  15516  isomninnlem  15520  iooref1o  15524  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  apdiff  15538  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542  dceqnconst  15550  dcapnconst  15551  nconstwlpolemgt0  15554  taupi  15563