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  2177  eqeq12i  2244  el2v  2807  vtocl2  2858  spc2ev  2901  sbc2ie  3102  csbieb  3168  sseq12i  3254  uneq12i  3358  ineq12i  3405  ifssun  3621  nelpri  3694  ralpr  3725  rexpr  3726  preq12i  3754  dfop  3862  opeq12i  3868  breq12i  4098  mpteq2ia  4176  exmidundif  4298  exmidundifim  4299  opex  4323  opi2  4327  opth2  4334  opeqsn  4347  opeqpr  4348  uniop  4350  opelopaba  4362  braba  4363  opelopab  4368  brab  4369  opelopabaf  4370  unex  4540  snnex  4547  op1stb  4577  ifelpwun  4582  ifex  4585  onun2i  4591  onsucssi  4606  ontriexmidim  4622  ontr2exmid  4625  onsucsssucexmid  4627  onsucelsucexmid  4630  opthreg  4656  tfis  4683  finds  4700  finds2  4701  nnregexmid  4721  xpeq12i  4749  opelvv  4778  eqrelriiv  4822  eqrelrdv  4824  xpss  4836  xpex  4844  relop  4882  brco  4903  opelcnv  4914  brcnv  4915  asymref  5124  codir  5127  ssrnres  5181  dmprop  5213  dfco2  5238  cossxp  5261  cocnvss  5264  coex  5284  funsn  5380  fnsn  5386  feq23i  5479  resasplitss  5518  fabex  5527  fvex  5662  xpsn  5827  fmptap  5847  opabex  5883  acexmidlemv  6021  oveq12i  6035  oprabid  6055  oprabss  6112  caovcom  6185  opabex3  6289  iunex  6290  oprabex  6295  ofmres  6303  op1st  6314  op2nd  6315  fo1st  6325  fo2nd  6326  mpoex  6384  1stconst  6391  2ndconst  6392  algrflem  6399  dftpos4  6434  tpostpos  6435  tpossym  6447  frecex  6565  frecfnom  6572  2oex  6604  sucinc  6618  fnoei  6625  oeiexg  6626  nnacli  6655  nnmcli  6656  elec  6748  ecovcom  6816  ecovass  6818  ecovdi  6820  fnmap  6829  mapval  6834  elmap  6851  elpm  6853  elpm2  6854  map0  6863  ixpconst  6882  entri  6965  endisj  7013  xpcomco  7015  phplem2  7044  1ndom2  7056  ssfiexmid  7068  domfiexmid  7072  exmidpw2en  7109  unfiexmid  7115  unfiin  7123  inresflem  7264  casefun  7289  caserel  7291  caseinj  7293  omp1eomlem  7298  omp1eom  7299  endjusym  7300  djufun  7308  djuinj  7310  ctssdccl  7315  ctssdclemr  7316  nninfex  7325  infnninf  7328  fodjuomnilemdc  7348  ctssexmid  7354  exmidonfinlem  7409  dju1p1e2  7413  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  exmidaclem  7428  pw1dom2  7450  onntri35  7460  onntri45  7464  2oneel  7480  2omotaplemst  7482  acnccim  7496  1lt2pi  7565  indpi  7567  1nq  7591  rec1nq  7620  1lt2nq  7631  ltaddnq  7632  halfnqq  7635  prarloclemarch2  7644  prarloclemlt  7718  prarloclemcalc  7727  genpelxp  7736  ltexprlempr  7833  recexprlempr  7857  cauappcvgprlemcl  7878  cauappcvgprlemladd  7883  caucvgprlemcl  7901  caucvgprprlemcl  7929  suplocexprlemell  7938  suplocexprlemdisj  7945  suplocexprlemub  7948  0r  7975  1sr  7976  m1r  7977  m1p1sr  7985  m1m1sr  7986  0lt1sr  7990  1ne0sr  7991  1idsr  7993  recexgt0sr  7998  prsradd  8011  caucvgsrlemoffres  8025  caucvgsr  8027  mappsrprg  8029  map2psrprg  8030  pitonnlem1p1  8071  pitonnlem2  8072  pitoregt0  8074  peano2nnnn  8078  axi2m1  8100  axprecex  8105  axcnre  8106  nnindnn  8118  nntopi  8119  0cn  8176  addcli  8188  mulcli  8189  mulcomi  8190  readdcli  8197  remulcli  8198  rexpssxrxp  8229  ltrelxr  8245  gtneii  8280  lttri3i  8282  letri3i  8283  ltnsymi  8284  lenlti  8285  ltlei  8286  mulgt0i  8294  mulgt0ii  8295  0lt1  8311  addcomi  8328  pncan3oi  8400  resubcli  8447  subcli  8460  pncan3i  8461  negsubi  8462  subnegi  8463  subeq0i  8464  neg11i  8465  negcon1i  8466  negcon2i  8467  mulneg1i  8588  mulneg2i  8589  mul2negi  8590  addgt0ii  8676  ltnegi  8678  lenegi  8679  ltnegcon2i  8680  lesub0i  8681  ltaddposi  8682  posdifi  8683  ltnegcon1i  8684  lenegcon1i  8685  subge0i  8686  1ap0  8775  ltapii  8820  recrecapi  8929  dividapi  8930  div0api  8931  rec11apii  8946  divdiv32api  8952  recgt0ii  9092  ltrecii  9103  ltdiv23ii  9112  sup3exmid  9142  nnssre  9152  nnind  9164  nnmulcli  9170  nnsubi  9188  0le2  9238  1lt3  9320  2lt4  9322  1lt4  9323  3lt5  9325  2lt5  9326  1lt5  9327  4lt6  9329  3lt6  9330  2lt6  9331  1lt6  9332  5lt7  9334  4lt7  9335  3lt7  9336  2lt7  9337  1lt7  9338  6lt8  9340  5lt8  9341  4lt8  9342  3lt8  9343  2lt8  9344  1lt8  9345  7lt9  9347  6lt9  9348  5lt9  9349  4lt9  9350  3lt9  9351  2lt9  9352  1lt9  9353  2muline0  9374  nn0addcli  9444  nn0mulcli  9445  nn0addge1i  9455  nn0addge2i  9456  dfz2  9557  halfnz  9581  9p1e10  9618  numnncl  9625  numltc  9641  le9lt10  9642  nummac  9660  8lt10  9747  7lt10  9748  6lt10  9749  5lt10  9750  4lt10  9751  3lt10  9752  2lt10  9753  1lt10  9754  eluzaddi  9788  eluzsubi  9789  uzuzle23  9801  uzuzle24  9802  uzuzle34  9803  eluz2nn  9805  eluz4eluz2  9807  eluzge3nn  9811  divfnzn  9860  elq  9861  qreccl  9881  xrltnr  10019  mnfltpnf  10025  xaddmnf1  10088  pnfaddmnf  10090  mnfaddpnf  10091  xrex  10096  xaddid1  10102  xsubge0  10121  xposdif  10122  xleaddadd  10127  elicc2i  10179  ioomax  10188  iccmax  10189  ioopos  10190  elxrge0  10218  iccshftri  10235  iccshftli  10237  iccdili  10239  icccntri  10241  unitssre  10245  fz10  10286  fzpreddisj  10311  fz0to4untppr  10364  dfrp2  10529  fldiv4p1lem1div2  10571  fldiv4lem1div2  10573  frecfzennn  10694  xnn0nnen  10705  fnn0nninf  10706  fxnn0nninf  10707  0tonninf  10708  1tonninf  10709  m1expcl2  10829  m1expcl  10830  nn0expcli  10833  sqmuli  10890  cu2  10906  i3  10909  subsqi  10917  binom2subi  10923  bcpasc  11034  4bc2eq6  11042  hashinfom  11046  prhash2ex  11079  hashp1i  11080  lsw0g  11171  swrdccat3blem  11329  rei  11482  imi  11483  readdi  11511  imaddi  11512  remuli  11513  immuli  11514  cjaddi  11515  cjmuli  11516  ipcni  11517  crrei  11519  crimi  11520  rexfiuz  11572  sqrt1  11629  sqrt4  11630  sqrt9  11631  abs1  11655  sqrtmulii  11717  abslti  11721  abslei  11722  abssubi  11733  absmuli  11734  sqabsaddi  11735  sqabssubi  11736  abstrii  11738  fimaxre2  11810  climz  11875  abscn2  11898  recn2  11900  imcn2  11901  climabs  11903  climre  11905  climim  11906  fsumcnv  12021  fsumrelem  12055  fsumre  12056  fsumim  12057  arisum2  12083  expcnv  12088  geo2sum2  12099  geo2lim  12100  0.999...  12105  geoihalfsum  12106  fprodcnv  12209  fprodge0  12221  fprodge1  12223  ege2le3  12255  ef0  12256  reeff1  12284  tan0  12315  ef01bndlem  12340  sin01bnd  12341  cos01bnd  12342  cos1bnd  12343  cos2bnd  12344  sinltxirr  12345  sin01gt0  12346  cos01gt0  12347  sin02gt0  12348  sincos1sgn  12349  sincos2sgn  12350  cos12dec  12352  egt2lt3  12364  epos  12365  ene1  12369  eap1  12370  3dvds  12448  3dvdsdec  12449  3dvds2dec  12450  odd2np1lem  12456  n2dvds1  12496  z4even  12500  ndvdsi  12517  flodddiv4  12520  bitsp1o  12537  0bits  12543  gcd0val  12554  6gcd4e2  12589  3lcm2e6woprm  12681  6lcm4e12  12682  3lcm2e6  12755  sqrt2irrlem  12756  phimullem  12820  pockthi  12954  4sqlem19  13005  dec2dvds  13007  dec5dvds2  13009  dec2nprm  13011  modxai  13012  gcdi  13016  gcdmodi  13017  numexpp1  13020  karatsuba  13026  2exp7  13030  xpnnen  13038  xpomen  13039  ennnfonelemj0  13045  ennnfonelem0  13049  ennnfonelemhf1o  13057  exmidunben  13070  qnnen  13075  unct  13086  setscom  13145  strleun  13210  prdsex  13375  prdsvallem  13378  imasival  13412  ismgm  13463  fn0g  13481  fngsum  13494  issgrp  13509  ismnddef  13524  isghm  13853  isrng  13971  rngmgpf  13974  isring  14037  mgpf  14048  dfrhm2  14192  rhmex  14195  isdomn  14307  rmodislmod  14389  lidlmex  14513  mopnset  14590  cnfldstr  14596  cnfldcj  14603  cnfld0  14609  cnfldplusf  14612  zringcrng  14630  zringmulr  14637  zringmpg  14644  znval  14674  psrval  14704  fnpsr  14705  fnmpl  14736  txtopi  15014  txunii  15017  upxp  15025  uptx  15027  cnmpt1st  15041  cnmpt2nd  15042  txswaphmeolem  15073  qtopbasss  15274  cnmet  15283  cnfldms  15289  cnopncntop  15297  cnopn  15298  remet  15301  blssioo  15306  tgqioo  15308  tgioo2cntop  15310  tgioo2  15312  divcnap  15318  abscncf  15338  recncf  15339  imcncf  15340  cjcncf  15341  mulc1cncf  15342  cncfcn1cntop  15347  idcncf  15354  cdivcncfap  15357  expcncf  15362  cnrehmeocntop  15363  maxcncf  15368  mincncf  15369  ivthreinc  15398  hovercncf  15399  limccnp2lem  15429  limccnp2cntop  15430  dvcnp2cntop  15452  dvaddxxbr  15454  dvmulxxbr  15455  dvcoapbr  15460  dvrecap  15466  dveflem  15479  dvef  15480  sincn  15522  coscn  15523  reeff1oleme  15525  reeff1o  15526  cosz12  15533  sin0pilem1  15534  sin0pilem2  15535  pipos  15541  sinhalfpilem  15544  sincosq1lem  15578  sincosq1sgn  15579  sincosq2sgn  15580  sincosq3sgn  15581  sincosq4sgn  15582  sinq12gt0  15583  cosq14gt0  15585  cosq23lt0  15586  coseq0q4123  15587  coseq00topi  15588  coseq0negpitopi  15589  tangtx  15591  sincos4thpi  15593  tan4thpi  15594  sincos6thpi  15595  pigt3  15597  cosordlem  15602  cosq34lt1  15603  cos02pilt1  15604  cos0pilt1  15605  ioocosf1o  15607  negpitopissre  15608  log1  15619  loge  15620  2logb9irr  15724  sqrt2cxp2logb9e3  15728  2logb9irrap  15730  mpodvdsmulf1o  15743  fsumdvdsmul  15744  1sgm2ppw  15748  lgsdir2lem2  15787  lgsdir2lem3  15788  lgseisenlem4  15831  2lgsoddprmlem3  15869  2sqlem9  15882  2sqlem10  15883  opvtxfvi  15907  opiedgfvi  15908  umgrbien  15990  usgrprc  16132  vtxdfifiun  16177  upgr2wlkdc  16257  konigsbergvtx  16362  konigsbergiedg  16363  konigsbergumgr  16367  konigsberglem1  16368  konigsberglem2  16369  konigsberglem3  16370  konigsberglem5  16372  konigsberg  16373  ex-fl  16378  ex-ceil  16379  ex-bc  16382  ex-dvds  16383  ex-gcd  16384  bj-charfunbi  16466  bj-unex  16574  bj-nn0suc0  16605  bj-nntrans  16606  bj-nnelirr  16608  012of  16652  2o01f  16653  pwle2  16659  nnsf  16670  peano3nninf  16672  exmidsbthrlem  16689  sbthom  16693  repiecelem  16696  repiecele0  16697  repiecege0  16698  isomninnlem  16701  iooref1o  16705  trilpolemisumle  16709  trilpolemeq1  16711  trilpolemlt1  16712  apdiff  16719  iswomninnlem  16721  iswomni0  16723  ismkvnnlem  16724  dceqnconst  16732  dcapnconst  16733  nconstwlpolemgt0  16736  taupi  16745