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  716  mp3an  1337  barbara  2124  eqeq12i  2191  vtocl2  2794  spc2ev  2835  sbc2ie  3036  csbieb  3100  sseq12i  3185  uneq12i  3289  ineq12i  3336  ifssun  3550  nelpri  3618  ralpr  3649  rexpr  3650  preq12i  3676  dfop  3779  opeq12i  3785  breq12i  4014  mpteq2ia  4091  exmidundif  4208  exmidundifim  4209  opex  4231  opi2  4235  opth2  4242  opeqsn  4254  opeqpr  4255  uniop  4257  opelopaba  4268  braba  4269  opelopab  4273  brab  4274  opelopabaf  4275  unex  4443  snnex  4450  op1stb  4480  ifelpwun  4485  onun2i  4492  onsucssi  4507  ontriexmidim  4523  ontr2exmid  4526  onsucsssucexmid  4528  onsucelsucexmid  4531  opthreg  4557  tfis  4584  finds  4601  finds2  4602  nnregexmid  4622  xpeq12i  4650  opelvv  4678  eqrelriiv  4722  eqrelrdv  4724  xpss  4736  xpex  4743  relop  4779  brco  4800  opelcnv  4811  brcnv  4812  asymref  5016  codir  5019  ssrnres  5073  dmprop  5105  dfco2  5130  cossxp  5153  cocnvss  5156  coex  5176  funsn  5266  fnsn  5272  feq23i  5362  resasplitss  5397  fabex  5406  fvex  5537  xpsn  5694  fmptap  5708  opabex  5742  acexmidlemv  5875  oveq12i  5889  oprabid  5909  oprabss  5963  caovcom  6034  opabex3  6125  iunex  6126  oprabex  6131  ofmres  6139  op1st  6149  op2nd  6150  fo1st  6160  fo2nd  6161  mpoex  6217  1stconst  6224  2ndconst  6225  algrflem  6232  dftpos4  6266  tpostpos  6267  tpossym  6279  frecex  6397  frecfnom  6404  sucinc  6448  fnoei  6455  oeiexg  6456  nnacli  6485  nnmcli  6486  elec  6576  ecovcom  6644  ecovass  6646  ecovdi  6648  fnmap  6657  mapval  6662  elmap  6679  elpm  6681  elpm2  6682  map0  6691  ixpconst  6710  entri  6788  endisj  6826  xpcomco  6828  phplem2  6855  ssfiexmid  6878  domfiexmid  6880  unfiexmid  6919  unfiin  6927  inresflem  7061  casefun  7086  caserel  7088  caseinj  7090  omp1eomlem  7095  omp1eom  7096  endjusym  7097  djufun  7105  djuinj  7107  ctssdccl  7112  ctssdclemr  7113  nninfex  7122  infnninf  7124  fodjuomnilemdc  7144  ctssexmid  7150  exmidonfinlem  7194  dju1p1e2  7198  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  pw1dom2  7228  onntri35  7238  onntri45  7242  2oneel  7257  2omotaplemst  7259  1lt2pi  7341  indpi  7343  1nq  7367  rec1nq  7396  1lt2nq  7407  ltaddnq  7408  halfnqq  7411  prarloclemarch2  7420  prarloclemlt  7494  prarloclemcalc  7503  genpelxp  7512  ltexprlempr  7609  recexprlempr  7633  cauappcvgprlemcl  7654  cauappcvgprlemladd  7659  caucvgprlemcl  7677  caucvgprprlemcl  7705  suplocexprlemell  7714  suplocexprlemdisj  7721  suplocexprlemub  7724  0r  7751  1sr  7752  m1r  7753  m1p1sr  7761  m1m1sr  7762  0lt1sr  7766  1ne0sr  7767  1idsr  7769  recexgt0sr  7774  prsradd  7787  caucvgsrlemoffres  7801  caucvgsr  7803  mappsrprg  7805  map2psrprg  7806  pitonnlem1p1  7847  pitonnlem2  7848  pitoregt0  7850  peano2nnnn  7854  axi2m1  7876  axprecex  7881  axcnre  7882  nnindnn  7894  nntopi  7895  0cn  7951  addcli  7963  mulcli  7964  mulcomi  7965  readdcli  7972  remulcli  7973  rexpssxrxp  8004  ltrelxr  8020  gtneii  8055  lttri3i  8057  letri3i  8058  ltnsymi  8059  lenlti  8060  ltlei  8061  mulgt0i  8069  mulgt0ii  8070  0lt1  8086  addcomi  8103  pncan3oi  8175  resubcli  8222  subcli  8235  pncan3i  8236  negsubi  8237  subnegi  8238  subeq0i  8239  neg11i  8240  negcon1i  8241  negcon2i  8242  mulneg1i  8363  mulneg2i  8364  mul2negi  8365  addgt0ii  8450  ltnegi  8452  lenegi  8453  ltnegcon2i  8454  lesub0i  8455  ltaddposi  8456  posdifi  8457  ltnegcon1i  8458  lenegcon1i  8459  subge0i  8460  1ap0  8549  ltapii  8594  recrecapi  8703  dividapi  8704  div0api  8705  rec11apii  8720  divdiv32api  8726  recgt0ii  8866  ltrecii  8877  ltdiv23ii  8886  sup3exmid  8916  nnssre  8925  nnind  8937  nnmulcli  8943  nnsubi  8961  0le2  9011  1lt3  9092  2lt4  9094  1lt4  9095  3lt5  9097  2lt5  9098  1lt5  9099  4lt6  9101  3lt6  9102  2lt6  9103  1lt6  9104  5lt7  9106  4lt7  9107  3lt7  9108  2lt7  9109  1lt7  9110  6lt8  9112  5lt8  9113  4lt8  9114  3lt8  9115  2lt8  9116  1lt8  9117  7lt9  9119  6lt9  9120  5lt9  9121  4lt9  9122  3lt9  9123  2lt9  9124  1lt9  9125  2muline0  9146  nn0addcli  9215  nn0mulcli  9216  nn0addge1i  9226  nn0addge2i  9227  dfz2  9327  halfnz  9351  9p1e10  9388  numnncl  9395  numltc  9411  le9lt10  9412  nummac  9430  8lt10  9517  7lt10  9518  6lt10  9519  5lt10  9520  4lt10  9521  3lt10  9522  2lt10  9523  1lt10  9524  eluzaddi  9556  eluzsubi  9557  eluz2nn  9568  eluz4eluz2  9569  uzuzle23  9573  eluzge3nn  9574  divfnzn  9623  elq  9624  qreccl  9644  xrltnr  9781  mnfltpnf  9787  xaddmnf1  9850  pnfaddmnf  9852  mnfaddpnf  9853  xrex  9858  xaddid1  9864  xsubge0  9883  xposdif  9884  xleaddadd  9889  elicc2i  9941  ioomax  9950  iccmax  9951  ioopos  9952  elxrge0  9980  iccshftri  9997  iccshftli  9999  iccdili  10001  icccntri  10003  unitssre  10007  fz10  10048  fzpreddisj  10073  fz0to4untppr  10126  dfrp2  10266  fldiv4p1lem1div2  10307  frecfzennn  10428  fnn0nninf  10439  fxnn0nninf  10440  0tonninf  10441  1tonninf  10442  m1expcl2  10544  m1expcl  10545  nn0expcli  10548  sqmuli  10605  cu2  10621  i3  10624  subsqi  10632  binom2subi  10638  bcpasc  10748  4bc2eq6  10756  hashinfom  10760  prhash2ex  10791  hashp1i  10792  rei  10910  imi  10911  readdi  10939  imaddi  10940  remuli  10941  immuli  10942  cjaddi  10943  cjmuli  10944  ipcni  10945  crrei  10947  crimi  10948  rexfiuz  11000  sqrt1  11057  sqrt4  11058  sqrt9  11059  abs1  11083  sqrtmulii  11145  abslti  11149  abslei  11150  abssubi  11161  absmuli  11162  sqabsaddi  11163  sqabssubi  11164  abstrii  11166  fimaxre2  11237  climz  11302  abscn2  11325  recn2  11327  imcn2  11328  climabs  11330  climre  11332  climim  11333  fsumcnv  11447  fsumrelem  11481  fsumre  11482  fsumim  11483  arisum2  11509  expcnv  11514  geo2sum2  11525  geo2lim  11526  0.999...  11531  geoihalfsum  11532  fprodcnv  11635  fprodge0  11647  fprodge1  11649  ege2le3  11681  ef0  11682  reeff1  11710  tan0  11741  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  cos1bnd  11769  cos2bnd  11770  sin01gt0  11771  cos01gt0  11772  sin02gt0  11773  sincos1sgn  11774  sincos2sgn  11775  cos12dec  11777  egt2lt3  11789  epos  11790  ene1  11794  eap1  11795  3dvdsdec  11872  3dvds2dec  11873  odd2np1lem  11879  n2dvds1  11919  z4even  11923  ndvdsi  11940  flodddiv4  11941  gcd0val  11963  6gcd4e2  11998  3lcm2e6woprm  12088  6lcm4e12  12089  3lcm2e6  12162  sqrt2irrlem  12163  phimullem  12227  pockthi  12358  xpnnen  12397  xpomen  12398  ennnfonelemj0  12404  ennnfonelem0  12408  ennnfonelemhf1o  12416  exmidunben  12429  qnnen  12434  unct  12445  setscom  12504  strleun  12565  prdsex  12723  imasival  12732  ismgm  12781  fn0g  12799  issgrp  12814  ismnddef  12824  isring  13188  mgpf  13199  rmodislmod  13446  cnfldstr  13496  cnfldcj  13501  cnfld0  13504  cnfldplusf  13507  zringcrng  13521  zringmulr  13528  zringmpg  13535  txtopi  13800  txunii  13803  upxp  13811  uptx  13813  cnmpt1st  13827  cnmpt2nd  13828  txswaphmeolem  13859  qtopbasss  14060  cnmet  14069  cnopncntop  14076  remet  14079  blssioo  14084  tgqioo  14086  tgioo2cntop  14088  divcnap  14094  abscncf  14111  recncf  14112  imcncf  14113  cjcncf  14114  mulc1cncf  14115  cncfcn1cntop  14120  cdivcncfap  14126  expcncf  14131  cnrehmeocntop  14132  limccnp2lem  14184  limccnp2cntop  14185  dvcnp2cntop  14202  dvaddxxbr  14204  dvmulxxbr  14205  dvcoapbr  14210  dvrecap  14216  dveflem  14226  dvef  14227  sincn  14229  coscn  14230  reeff1oleme  14232  reeff1o  14233  cosz12  14240  sin0pilem1  14241  sin0pilem2  14242  pipos  14248  sinhalfpilem  14251  sincosq1lem  14285  sincosq1sgn  14286  sincosq2sgn  14287  sincosq3sgn  14288  sincosq4sgn  14289  sinq12gt0  14290  cosq14gt0  14292  cosq23lt0  14293  coseq0q4123  14294  coseq00topi  14295  coseq0negpitopi  14296  tangtx  14298  sincos4thpi  14300  tan4thpi  14301  sincos6thpi  14302  pigt3  14304  cosordlem  14309  cosq34lt1  14310  cos02pilt1  14311  cos0pilt1  14312  ioocosf1o  14314  negpitopissre  14315  log1  14326  loge  14327  2logb9irr  14428  sqrt2cxp2logb9e3  14432  2logb9irrap  14434  lgsdir2lem2  14469  lgsdir2lem3  14470  2lgsoddprmlem3  14498  2sqlem9  14510  2sqlem10  14511  ex-fl  14516  ex-ceil  14517  ex-bc  14520  ex-dvds  14521  ex-gcd  14522  bj-charfunbi  14602  bj-unex  14710  bj-nn0suc0  14741  bj-nntrans  14742  bj-nnelirr  14744  012of  14784  2o01f  14785  pwle2  14787  nnsf  14793  peano3nninf  14795  exmidsbthrlem  14809  sbthom  14813  isomninnlem  14817  iooref1o  14821  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  apdiff  14835  iswomninnlem  14836  iswomni0  14838  ismkvnnlem  14839  dceqnconst  14846  dcapnconst  14847  nconstwlpolemgt0  14850  taupi  14859