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  724  mp3an  1374  barbara  2181  eqeq12i  2248  el2v  2821  vtocl2  2872  spc2ev  2915  sbc2ie  3116  csbieb  3182  sseq12i  3268  uneq12i  3373  ineq12i  3422  ifssun  3639  nelpri  3715  ralpr  3746  rexpr  3747  preq12i  3775  dfop  3884  opeq12i  3890  breq12i  4120  mpteq2ia  4198  exmidundif  4321  exmidundifim  4322  opex  4347  opi2  4351  opth2  4358  opeqsn  4371  opeqpr  4372  uniop  4374  opelopaba  4386  braba  4387  opelopab  4392  brab  4393  opelopabaf  4394  unex  4564  snnex  4571  op1stb  4601  ifelpwun  4606  ifex  4609  onun2i  4615  onsucssi  4630  ontriexmidim  4646  ontr2exmid  4649  onsucsssucexmid  4651  onsucelsucexmid  4654  opthreg  4680  tfis  4707  finds  4724  finds2  4725  nnregexmid  4745  xpeq12i  4773  opelvv  4802  eqrelriiv  4846  eqrelrdv  4848  xpss  4860  xpex  4868  relop  4907  brco  4928  opelcnv  4939  brcnv  4940  asymref  5150  codir  5153  ssrnres  5207  dmprop  5239  dfco2  5264  cossxp  5287  cocnvss  5290  coex  5310  funsn  5406  fnsn  5412  feq23i  5505  resasplitss  5546  fabex  5557  fvex  5692  xpsn  5856  fmptap  5876  opabex  5912  acexmidlemv  6050  oveq12i  6064  oprabid  6084  oprabss  6141  caovcom  6214  opabex3  6317  iunex  6318  oprabex  6323  ofmres  6331  op1st  6342  op2nd  6343  fo1st  6353  fo2nd  6354  mpoex  6412  1stconst  6419  2ndconst  6420  algrflem  6427  dftpos4  6496  tpostpos  6497  tpossym  6509  frecex  6627  frecfnom  6634  2oex  6666  sucinc  6680  fnoei  6687  oeiexg  6688  nnacli  6717  nnmcli  6718  elec  6810  ecovcom  6878  ecovass  6880  ecovdi  6882  fnmap  6891  mapval  6896  elmap  6913  elpm  6915  elpm2  6916  map0  6926  ixpconst  6945  entri  7028  endisj  7077  xpcomco  7079  phplem2  7109  1ndom2  7121  ssfiexmid  7133  domfiexmid  7137  exmidpw2en  7174  unfiexmid  7180  unfiin  7188  inresflem  7353  casefun  7378  caserel  7380  caseinj  7382  omp1eomlem  7387  omp1eom  7388  endjusym  7389  djufun  7397  djuinj  7399  ctssdccl  7404  ctssdclemr  7405  nninfex  7414  infnninf  7417  fodjuomnilemdc  7437  ctssexmid  7443  exmidonfinlem  7498  dju1p1e2  7502  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  exmidaclem  7517  pw1dom2  7539  onntri35  7549  onntri45  7553  2oneel  7575  2omotaplemst  7577  acnccim  7591  1lt2pi  7660  indpi  7662  1nq  7686  rec1nq  7715  1lt2nq  7726  ltaddnq  7727  halfnqq  7730  prarloclemarch2  7739  prarloclemlt  7813  prarloclemcalc  7822  genpelxp  7831  ltexprlempr  7928  recexprlempr  7952  cauappcvgprlemcl  7973  cauappcvgprlemladd  7978  caucvgprlemcl  7996  caucvgprprlemcl  8024  suplocexprlemell  8033  suplocexprlemdisj  8040  suplocexprlemub  8043  0r  8070  1sr  8071  m1r  8072  m1p1sr  8080  m1m1sr  8081  0lt1sr  8085  1ne0sr  8086  1idsr  8088  recexgt0sr  8093  prsradd  8106  caucvgsrlemoffres  8120  caucvgsr  8122  mappsrprg  8124  map2psrprg  8125  pitonnlem1p1  8166  pitonnlem2  8167  pitoregt0  8169  peano2nnnn  8173  axi2m1  8195  axprecex  8200  axcnre  8201  nnindnn  8213  nntopi  8214  0cn  8271  addcli  8283  mulcli  8284  mulcomi  8285  readdcli  8292  remulcli  8293  rexpssxrxp  8323  ltrelxr  8339  gtneii  8374  lttri3i  8376  letri3i  8377  ltnsymi  8378  lenlti  8379  ltlei  8380  mulgt0i  8388  mulgt0ii  8389  0lt1  8405  addcomi  8422  pncan3oi  8494  resubcli  8541  subcli  8554  pncan3i  8555  negsubi  8556  subnegi  8557  subeq0i  8558  neg11i  8559  negcon1i  8560  negcon2i  8561  mulneg1i  8682  mulneg2i  8683  mul2negi  8684  addgt0ii  8770  ltnegi  8772  lenegi  8773  ltnegcon2i  8774  lesub0i  8775  ltaddposi  8776  posdifi  8777  ltnegcon1i  8778  lenegcon1i  8779  subge0i  8780  1ap0  8869  ltapii  8914  recrecapi  9023  dividapi  9024  div0api  9025  rec11apii  9040  divdiv32api  9046  recgt0ii  9186  ltrecii  9197  ltdiv23ii  9206  sup3exmid  9236  nnssre  9246  nnind  9258  nnmulcli  9264  nnsubi  9282  0le2  9332  1lt3  9414  2lt4  9416  1lt4  9417  3lt5  9419  2lt5  9420  1lt5  9421  4lt6  9423  3lt6  9424  2lt6  9425  1lt6  9426  5lt7  9428  4lt7  9429  3lt7  9430  2lt7  9431  1lt7  9432  6lt8  9434  5lt8  9435  4lt8  9436  3lt8  9437  2lt8  9438  1lt8  9439  7lt9  9441  6lt9  9442  5lt9  9443  4lt9  9444  3lt9  9445  2lt9  9446  1lt9  9447  2muline0  9468  nn0addcli  9538  nn0mulcli  9539  nn0addge1i  9549  nn0addge2i  9550  dfz2  9655  halfnz  9680  9p1e10  9717  numnncl  9724  numltc  9740  le9lt10  9741  nummac  9759  8lt10  9846  7lt10  9847  6lt10  9848  5lt10  9849  4lt10  9850  3lt10  9851  2lt10  9852  1lt10  9853  eluzaddi  9887  eluzsubi  9888  uzuzle23  9900  uzuzle24  9901  uzuzle34  9902  eluz2nn  9904  eluz4eluz2  9906  eluzge3nn  9910  divfnzn  9959  elq  9960  qreccl  9980  xrltnr  10118  mnfltpnf  10124  xaddmnf1  10187  pnfaddmnf  10189  mnfaddpnf  10190  xrex  10195  xaddid1  10201  xsubge0  10220  xposdif  10221  xleaddadd  10226  elicc2i  10278  ioomax  10287  iccmax  10288  ioopos  10289  elxrge0  10317  iccshftri  10334  iccshftli  10336  iccdili  10338  icccntri  10340  unitssre  10345  fz10  10386  fzpreddisj  10412  fz0to4untppr  10465  dfrp2  10630  fldiv4p1lem1div2  10672  fldiv4lem1div2  10674  frecfzennn  10795  xnn0nnen  10806  fnn0nninf  10807  fxnn0nninf  10808  0tonninf  10809  1tonninf  10810  m1expcl2  10930  m1expcl  10931  nn0expcli  10934  sqmuli  10991  cu2  11007  i3  11010  subsqi  11018  binom2subi  11024  bcpasc  11136  4bc2eq6  11145  hashinfom  11149  prhash2ex  11182  hashp1i  11183  lsw0g  11281  swrdccat3blem  11439  rei  11592  imi  11593  readdi  11621  imaddi  11622  remuli  11623  immuli  11624  cjaddi  11625  cjmuli  11626  ipcni  11627  crrei  11629  crimi  11630  rexfiuz  11682  sqrt1  11739  sqrt4  11740  sqrt9  11741  abs1  11765  sqrtmulii  11827  abslti  11831  abslei  11832  abssubi  11843  absmuli  11844  sqabsaddi  11845  sqabssubi  11846  abstrii  11848  fimaxre2  11920  climz  11985  abscn2  12008  recn2  12010  imcn2  12011  climabs  12013  climre  12015  climim  12016  fsumcnv  12131  fsumrelem  12165  fsumre  12166  fsumim  12167  arisum2  12193  expcnv  12198  geo2sum2  12209  geo2lim  12210  0.999...  12215  geoihalfsum  12216  fprodcnv  12319  fprodge0  12331  fprodge1  12333  ege2le3  12365  ef0  12366  reeff1  12394  tan0  12425  ef01bndlem  12450  sin01bnd  12451  cos01bnd  12452  cos1bnd  12453  cos2bnd  12454  sinltxirr  12455  sin01gt0  12456  cos01gt0  12457  sin02gt0  12458  sincos1sgn  12459  sincos2sgn  12460  cos12dec  12462  egt2lt3  12474  epos  12475  ene1  12479  eap1  12480  3dvds  12558  3dvdsdec  12559  3dvds2dec  12560  odd2np1lem  12566  n2dvds1  12606  z4even  12610  ndvdsi  12627  flodddiv4  12630  bitsp1o  12647  0bits  12653  gcd0val  12664  6gcd4e2  12699  3lcm2e6woprm  12791  6lcm4e12  12792  3lcm2e6  12865  sqrt2irrlem  12866  phimullem  12930  pockthi  13064  4sqlem19  13115  dec2dvds  13117  dec5dvds2  13119  dec2nprm  13121  modxai  13122  gcdi  13126  gcdmodi  13127  numexpp1  13130  karatsuba  13136  2exp7  13140  ballotfilemofi  13146  ballotfilem1  13147  ballotfilem2  13153  ballotfilemfmpn  13159  ballotfilemodife  13162  ballotfilem4  13163  xpnnen  13166  xpomen  13167  ennnfonelemj0  13173  ennnfonelem0  13177  ennnfonelemhf1o  13185  exmidunben  13198  qnnen  13203  unct  13214  setscom  13273  strleun  13338  prdsex  13503  prdsvallem  13506  imasival  13540  ismgm  13591  fn0g  13609  fngsum  13622  issgrp  13637  ismnddef  13652  isghm  13981  isrng  14099  rngmgpf  14102  isring  14165  mgpf  14176  dfrhm2  14321  rhmex  14324  isdomn  14438  rmodislmod  14548  lidlmex  14672  mopnset  14749  cnfldstr  14755  cnfldcj  14762  cnfld0  14768  cnfldplusf  14771  zringcrng  14789  zringmulr  14796  zringmpg  14803  znval  14833  psrval  14863  fnpsr  14864  fnmpl  14897  txtopi  15175  txunii  15178  upxp  15186  uptx  15188  cnmpt1st  15202  cnmpt2nd  15203  txswaphmeolem  15234  qtopbasss  15435  cnmet  15444  cnfldms  15450  cnopncntop  15458  cnopn  15459  remet  15462  blssioo  15467  tgqioo  15469  tgioo2cntop  15471  tgioo2  15473  divcnap  15479  abscncf  15499  recncf  15500  imcncf  15501  cjcncf  15502  mulc1cncf  15503  cncfcn1cntop  15508  idcncf  15515  cdivcncfap  15518  expcncf  15523  cnrehmeocntop  15524  maxcncf  15529  mincncf  15530  ivthreinc  15559  hovercncf  15560  limccnp2lem  15590  limccnp2cntop  15591  dvcnp2cntop  15613  dvaddxxbr  15615  dvmulxxbr  15616  dvcoapbr  15621  dvrecap  15627  dveflem  15640  dvef  15641  sincn  15683  coscn  15684  reeff1oleme  15686  reeff1o  15687  cosz12  15694  sin0pilem1  15695  sin0pilem2  15696  pipos  15702  sinhalfpilem  15705  sincosq1lem  15739  sincosq1sgn  15740  sincosq2sgn  15741  sincosq3sgn  15742  sincosq4sgn  15743  sinq12gt0  15744  cosq14gt0  15746  cosq23lt0  15747  coseq0q4123  15748  coseq00topi  15749  coseq0negpitopi  15750  tangtx  15752  sincos4thpi  15754  tan4thpi  15755  sincos6thpi  15756  pigt3  15758  cosordlem  15763  cosq34lt1  15764  cos02pilt1  15765  cos0pilt1  15766  ioocosf1o  15768  negpitopissre  15769  log1  15780  loge  15781  2logb9irr  15885  sqrt2cxp2logb9e3  15889  2logb9irrap  15891  mpodvdsmulf1o  15907  fsumdvdsmul  15908  1sgm2ppw  15912  lgsdir2lem2  15951  lgsdir2lem3  15952  lgseisenlem4  15995  2lgsoddprmlem3  16033  2sqlem9  16046  2sqlem10  16047  opvtxfvi  16071  opiedgfvi  16072  umgrbien  16154  usgrprc  16296  vtxdfifiun  16341  upgr2wlkdc  16421  konigsbergvtx  16526  konigsbergiedg  16527  konigsbergumgr  16531  konigsberglem1  16532  konigsberglem2  16533  konigsberglem3  16534  konigsberglem5  16536  konigsberg  16537  ex-fl  16542  ex-ceil  16543  ex-bc  16546  ex-dvds  16547  ex-gcd  16548  bj-charfunbi  16630  bj-unex  16738  bj-nn0suc0  16769  bj-nntrans  16770  bj-nnelirr  16772  012of  16816  2o01f  16817  pwle2  16821  nnsf  16832  peano3nninf  16834  exmidsbthrlem  16851  sbthom  16855  repiecelem  16858  repiecele0  16859  repiecege0  16860  isomninnlem  16863  iooref1o  16867  trilpolemisumle  16871  trilpolemeq1  16873  trilpolemlt1  16874  apdiff  16881  iswomninnlem  16883  iswomni0  16885  ismkvnnlem  16886  dceqnconst  16895  dcapnconst  16896  nconstwlpolemgt0  16899  taupi  16908