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  7272  dju1p1e2  7276  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  pw1dom2  7310  onntri35  7320  onntri45  7324  2oneel  7339  2omotaplemst  7341  acnccim  7355  1lt2pi  7424  indpi  7426  1nq  7450  rec1nq  7479  1lt2nq  7490  ltaddnq  7491  halfnqq  7494  prarloclemarch2  7503  prarloclemlt  7577  prarloclemcalc  7586  genpelxp  7595  ltexprlempr  7692  recexprlempr  7716  cauappcvgprlemcl  7737  cauappcvgprlemladd  7742  caucvgprlemcl  7760  caucvgprprlemcl  7788  suplocexprlemell  7797  suplocexprlemdisj  7804  suplocexprlemub  7807  0r  7834  1sr  7835  m1r  7836  m1p1sr  7844  m1m1sr  7845  0lt1sr  7849  1ne0sr  7850  1idsr  7852  recexgt0sr  7857  prsradd  7870  caucvgsrlemoffres  7884  caucvgsr  7886  mappsrprg  7888  map2psrprg  7889  pitonnlem1p1  7930  pitonnlem2  7931  pitoregt0  7933  peano2nnnn  7937  axi2m1  7959  axprecex  7964  axcnre  7965  nnindnn  7977  nntopi  7978  0cn  8035  addcli  8047  mulcli  8048  mulcomi  8049  readdcli  8056  remulcli  8057  rexpssxrxp  8088  ltrelxr  8104  gtneii  8139  lttri3i  8141  letri3i  8142  ltnsymi  8143  lenlti  8144  ltlei  8145  mulgt0i  8153  mulgt0ii  8154  0lt1  8170  addcomi  8187  pncan3oi  8259  resubcli  8306  subcli  8319  pncan3i  8320  negsubi  8321  subnegi  8322  subeq0i  8323  neg11i  8324  negcon1i  8325  negcon2i  8326  mulneg1i  8447  mulneg2i  8448  mul2negi  8449  addgt0ii  8535  ltnegi  8537  lenegi  8538  ltnegcon2i  8539  lesub0i  8540  ltaddposi  8541  posdifi  8542  ltnegcon1i  8543  lenegcon1i  8544  subge0i  8545  1ap0  8634  ltapii  8679  recrecapi  8788  dividapi  8789  div0api  8790  rec11apii  8805  divdiv32api  8811  recgt0ii  8951  ltrecii  8962  ltdiv23ii  8971  sup3exmid  9001  nnssre  9011  nnind  9023  nnmulcli  9029  nnsubi  9047  0le2  9097  1lt3  9179  2lt4  9181  1lt4  9182  3lt5  9184  2lt5  9185  1lt5  9186  4lt6  9188  3lt6  9189  2lt6  9190  1lt6  9191  5lt7  9193  4lt7  9194  3lt7  9195  2lt7  9196  1lt7  9197  6lt8  9199  5lt8  9200  4lt8  9201  3lt8  9202  2lt8  9203  1lt8  9204  7lt9  9206  6lt9  9207  5lt9  9208  4lt9  9209  3lt9  9210  2lt9  9211  1lt9  9212  2muline0  9233  nn0addcli  9303  nn0mulcli  9304  nn0addge1i  9314  nn0addge2i  9315  dfz2  9415  halfnz  9439  9p1e10  9476  numnncl  9483  numltc  9499  le9lt10  9500  nummac  9518  8lt10  9605  7lt10  9606  6lt10  9607  5lt10  9608  4lt10  9609  3lt10  9610  2lt10  9611  1lt10  9612  eluzaddi  9645  eluzsubi  9646  eluz2nn  9657  eluz4eluz2  9658  uzuzle23  9662  eluzge3nn  9663  divfnzn  9712  elq  9713  qreccl  9733  xrltnr  9871  mnfltpnf  9877  xaddmnf1  9940  pnfaddmnf  9942  mnfaddpnf  9943  xrex  9948  xaddid1  9954  xsubge0  9973  xposdif  9974  xleaddadd  9979  elicc2i  10031  ioomax  10040  iccmax  10041  ioopos  10042  elxrge0  10070  iccshftri  10087  iccshftli  10089  iccdili  10091  icccntri  10093  unitssre  10097  fz10  10138  fzpreddisj  10163  fz0to4untppr  10216  dfrp2  10370  fldiv4p1lem1div2  10412  fldiv4lem1div2  10414  frecfzennn  10535  xnn0nnen  10546  fnn0nninf  10547  fxnn0nninf  10548  0tonninf  10549  1tonninf  10550  m1expcl2  10670  m1expcl  10671  nn0expcli  10674  sqmuli  10731  cu2  10747  i3  10750  subsqi  10758  binom2subi  10764  bcpasc  10875  4bc2eq6  10883  hashinfom  10887  prhash2ex  10918  hashp1i  10919  rei  11081  imi  11082  readdi  11110  imaddi  11111  remuli  11112  immuli  11113  cjaddi  11114  cjmuli  11115  ipcni  11116  crrei  11118  crimi  11119  rexfiuz  11171  sqrt1  11228  sqrt4  11229  sqrt9  11230  abs1  11254  sqrtmulii  11316  abslti  11320  abslei  11321  abssubi  11332  absmuli  11333  sqabsaddi  11334  sqabssubi  11335  abstrii  11337  fimaxre2  11409  climz  11474  abscn2  11497  recn2  11499  imcn2  11500  climabs  11502  climre  11504  climim  11505  fsumcnv  11619  fsumrelem  11653  fsumre  11654  fsumim  11655  arisum2  11681  expcnv  11686  geo2sum2  11697  geo2lim  11698  0.999...  11703  geoihalfsum  11704  fprodcnv  11807  fprodge0  11819  fprodge1  11821  ege2le3  11853  ef0  11854  reeff1  11882  tan0  11913  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  cos1bnd  11941  cos2bnd  11942  sinltxirr  11943  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  sincos1sgn  11947  sincos2sgn  11948  cos12dec  11950  egt2lt3  11962  epos  11963  ene1  11967  eap1  11968  3dvds  12046  3dvdsdec  12047  3dvds2dec  12048  odd2np1lem  12054  n2dvds1  12094  z4even  12098  ndvdsi  12115  flodddiv4  12118  bitsp1o  12135  0bits  12141  gcd0val  12152  6gcd4e2  12187  3lcm2e6woprm  12279  6lcm4e12  12280  3lcm2e6  12353  sqrt2irrlem  12354  phimullem  12418  pockthi  12552  4sqlem19  12603  dec2dvds  12605  dec5dvds2  12607  dec2nprm  12609  modxai  12610  gcdi  12614  gcdmodi  12615  numexpp1  12618  karatsuba  12624  2exp7  12628  xpnnen  12636  xpomen  12637  ennnfonelemj0  12643  ennnfonelem0  12647  ennnfonelemhf1o  12655  exmidunben  12668  qnnen  12673  unct  12684  setscom  12743  strleun  12807  prdsex  12971  prdsvallem  12974  imasival  13008  ismgm  13059  fn0g  13077  fngsum  13090  issgrp  13105  ismnddef  13120  isghm  13449  isrng  13566  rngmgpf  13569  isring  13632  mgpf  13643  dfrhm2  13786  rhmex  13789  isdomn  13901  rmodislmod  13983  lidlmex  14107  mopnset  14184  cnfldstr  14190  cnfldcj  14197  cnfld0  14203  cnfldplusf  14206  zringcrng  14224  zringmulr  14231  zringmpg  14238  znval  14268  psrval  14296  fnpsr  14297  txtopi  14581  txunii  14584  upxp  14592  uptx  14594  cnmpt1st  14608  cnmpt2nd  14609  txswaphmeolem  14640  qtopbasss  14841  cnmet  14850  cnfldms  14856  cnopncntop  14864  cnopn  14865  remet  14868  blssioo  14873  tgqioo  14875  tgioo2cntop  14877  tgioo2  14879  divcnap  14885  abscncf  14905  recncf  14906  imcncf  14907  cjcncf  14908  mulc1cncf  14909  cncfcn1cntop  14914  idcncf  14921  cdivcncfap  14924  expcncf  14929  cnrehmeocntop  14930  maxcncf  14935  mincncf  14936  ivthreinc  14965  hovercncf  14966  limccnp2lem  14996  limccnp2cntop  14997  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvrecap  15033  dveflem  15046  dvef  15047  sincn  15089  coscn  15090  reeff1oleme  15092  reeff1o  15093  cosz12  15100  sin0pilem1  15101  sin0pilem2  15102  pipos  15108  sinhalfpilem  15111  sincosq1lem  15145  sincosq1sgn  15146  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  cosq14gt0  15152  cosq23lt0  15153  coseq0q4123  15154  coseq00topi  15155  coseq0negpitopi  15156  tangtx  15158  sincos4thpi  15160  tan4thpi  15161  sincos6thpi  15162  pigt3  15164  cosordlem  15169  cosq34lt1  15170  cos02pilt1  15171  cos0pilt1  15172  ioocosf1o  15174  negpitopissre  15175  log1  15186  loge  15187  2logb9irr  15291  sqrt2cxp2logb9e3  15295  2logb9irrap  15297  mpodvdsmulf1o  15310  fsumdvdsmul  15311  1sgm2ppw  15315  lgsdir2lem2  15354  lgsdir2lem3  15355  lgseisenlem4  15398  2lgsoddprmlem3  15436  2sqlem9  15449  2sqlem10  15450  ex-fl  15455  ex-ceil  15456  ex-bc  15459  ex-dvds  15460  ex-gcd  15461  bj-charfunbi  15541  bj-unex  15649  bj-nn0suc0  15680  bj-nntrans  15681  bj-nnelirr  15683  012of  15724  2o01f  15725  pwle2  15729  nnsf  15736  peano3nninf  15738  exmidsbthrlem  15753  sbthom  15757  isomninnlem  15761  iooref1o  15765  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  apdiff  15779  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783  dceqnconst  15791  dcapnconst  15792  nconstwlpolemgt0  15795  taupi  15804