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  721  mp3an  1371  barbara  2176  eqeq12i  2243  el2v  2806  vtocl2  2857  spc2ev  2900  sbc2ie  3101  csbieb  3167  sseq12i  3253  uneq12i  3357  ineq12i  3404  ifssun  3618  nelpri  3691  ralpr  3722  rexpr  3723  preq12i  3751  dfop  3859  opeq12i  3865  breq12i  4095  mpteq2ia  4173  exmidundif  4294  exmidundifim  4295  opex  4319  opi2  4323  opth2  4330  opeqsn  4343  opeqpr  4344  uniop  4346  opelopaba  4358  braba  4359  opelopab  4364  brab  4365  opelopabaf  4366  unex  4536  snnex  4543  op1stb  4573  ifelpwun  4578  ifex  4581  onun2i  4587  onsucssi  4602  ontriexmidim  4618  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmid  4626  opthreg  4652  tfis  4679  finds  4696  finds2  4697  nnregexmid  4717  xpeq12i  4745  opelvv  4774  eqrelriiv  4818  eqrelrdv  4820  xpss  4832  xpex  4840  relop  4878  brco  4899  opelcnv  4910  brcnv  4911  asymref  5120  codir  5123  ssrnres  5177  dmprop  5209  dfco2  5234  cossxp  5257  cocnvss  5260  coex  5280  funsn  5375  fnsn  5381  feq23i  5474  resasplitss  5513  fabex  5522  fvex  5655  xpsn  5819  fmptap  5839  opabex  5873  acexmidlemv  6011  oveq12i  6025  oprabid  6045  oprabss  6102  caovcom  6175  opabex3  6279  iunex  6280  oprabex  6285  ofmres  6293  op1st  6304  op2nd  6305  fo1st  6315  fo2nd  6316  mpoex  6374  1stconst  6381  2ndconst  6382  algrflem  6389  dftpos4  6424  tpostpos  6425  tpossym  6437  frecex  6555  frecfnom  6562  2oex  6594  sucinc  6608  fnoei  6615  oeiexg  6616  nnacli  6645  nnmcli  6646  elec  6738  ecovcom  6806  ecovass  6808  ecovdi  6810  fnmap  6819  mapval  6824  elmap  6841  elpm  6843  elpm2  6844  map0  6853  ixpconst  6872  entri  6955  endisj  7003  xpcomco  7005  phplem2  7034  1ndom2  7046  ssfiexmid  7058  domfiexmid  7062  exmidpw2en  7099  unfiexmid  7105  unfiin  7113  inresflem  7253  casefun  7278  caserel  7280  caseinj  7282  omp1eomlem  7287  omp1eom  7288  endjusym  7289  djufun  7297  djuinj  7299  ctssdccl  7304  ctssdclemr  7305  nninfex  7314  infnninf  7317  fodjuomnilemdc  7337  ctssexmid  7343  exmidonfinlem  7397  dju1p1e2  7401  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  exmidaclem  7416  pw1dom2  7438  onntri35  7448  onntri45  7452  2oneel  7468  2omotaplemst  7470  acnccim  7484  1lt2pi  7553  indpi  7555  1nq  7579  rec1nq  7608  1lt2nq  7619  ltaddnq  7620  halfnqq  7623  prarloclemarch2  7632  prarloclemlt  7706  prarloclemcalc  7715  genpelxp  7724  ltexprlempr  7821  recexprlempr  7845  cauappcvgprlemcl  7866  cauappcvgprlemladd  7871  caucvgprlemcl  7889  caucvgprprlemcl  7917  suplocexprlemell  7926  suplocexprlemdisj  7933  suplocexprlemub  7936  0r  7963  1sr  7964  m1r  7965  m1p1sr  7973  m1m1sr  7974  0lt1sr  7978  1ne0sr  7979  1idsr  7981  recexgt0sr  7986  prsradd  7999  caucvgsrlemoffres  8013  caucvgsr  8015  mappsrprg  8017  map2psrprg  8018  pitonnlem1p1  8059  pitonnlem2  8060  pitoregt0  8062  peano2nnnn  8066  axi2m1  8088  axprecex  8093  axcnre  8094  nnindnn  8106  nntopi  8107  0cn  8164  addcli  8176  mulcli  8177  mulcomi  8178  readdcli  8185  remulcli  8186  rexpssxrxp  8217  ltrelxr  8233  gtneii  8268  lttri3i  8270  letri3i  8271  ltnsymi  8272  lenlti  8273  ltlei  8274  mulgt0i  8282  mulgt0ii  8283  0lt1  8299  addcomi  8316  pncan3oi  8388  resubcli  8435  subcli  8448  pncan3i  8449  negsubi  8450  subnegi  8451  subeq0i  8452  neg11i  8453  negcon1i  8454  negcon2i  8455  mulneg1i  8576  mulneg2i  8577  mul2negi  8578  addgt0ii  8664  ltnegi  8666  lenegi  8667  ltnegcon2i  8668  lesub0i  8669  ltaddposi  8670  posdifi  8671  ltnegcon1i  8672  lenegcon1i  8673  subge0i  8674  1ap0  8763  ltapii  8808  recrecapi  8917  dividapi  8918  div0api  8919  rec11apii  8934  divdiv32api  8940  recgt0ii  9080  ltrecii  9091  ltdiv23ii  9100  sup3exmid  9130  nnssre  9140  nnind  9152  nnmulcli  9158  nnsubi  9176  0le2  9226  1lt3  9308  2lt4  9310  1lt4  9311  3lt5  9313  2lt5  9314  1lt5  9315  4lt6  9317  3lt6  9318  2lt6  9319  1lt6  9320  5lt7  9322  4lt7  9323  3lt7  9324  2lt7  9325  1lt7  9326  6lt8  9328  5lt8  9329  4lt8  9330  3lt8  9331  2lt8  9332  1lt8  9333  7lt9  9335  6lt9  9336  5lt9  9337  4lt9  9338  3lt9  9339  2lt9  9340  1lt9  9341  2muline0  9362  nn0addcli  9432  nn0mulcli  9433  nn0addge1i  9443  nn0addge2i  9444  dfz2  9545  halfnz  9569  9p1e10  9606  numnncl  9613  numltc  9629  le9lt10  9630  nummac  9648  8lt10  9735  7lt10  9736  6lt10  9737  5lt10  9738  4lt10  9739  3lt10  9740  2lt10  9741  1lt10  9742  eluzaddi  9776  eluzsubi  9777  uzuzle23  9789  uzuzle24  9790  uzuzle34  9791  eluz2nn  9793  eluz4eluz2  9795  eluzge3nn  9799  divfnzn  9848  elq  9849  qreccl  9869  xrltnr  10007  mnfltpnf  10013  xaddmnf1  10076  pnfaddmnf  10078  mnfaddpnf  10079  xrex  10084  xaddid1  10090  xsubge0  10109  xposdif  10110  xleaddadd  10115  elicc2i  10167  ioomax  10176  iccmax  10177  ioopos  10178  elxrge0  10206  iccshftri  10223  iccshftli  10225  iccdili  10227  icccntri  10229  unitssre  10233  fz10  10274  fzpreddisj  10299  fz0to4untppr  10352  dfrp2  10516  fldiv4p1lem1div2  10558  fldiv4lem1div2  10560  frecfzennn  10681  xnn0nnen  10692  fnn0nninf  10693  fxnn0nninf  10694  0tonninf  10695  1tonninf  10696  m1expcl2  10816  m1expcl  10817  nn0expcli  10820  sqmuli  10877  cu2  10893  i3  10896  subsqi  10904  binom2subi  10910  bcpasc  11021  4bc2eq6  11029  hashinfom  11033  prhash2ex  11066  hashp1i  11067  lsw0g  11155  swrdccat3blem  11313  rei  11453  imi  11454  readdi  11482  imaddi  11483  remuli  11484  immuli  11485  cjaddi  11486  cjmuli  11487  ipcni  11488  crrei  11490  crimi  11491  rexfiuz  11543  sqrt1  11600  sqrt4  11601  sqrt9  11602  abs1  11626  sqrtmulii  11688  abslti  11692  abslei  11693  abssubi  11704  absmuli  11705  sqabsaddi  11706  sqabssubi  11707  abstrii  11709  fimaxre2  11781  climz  11846  abscn2  11869  recn2  11871  imcn2  11872  climabs  11874  climre  11876  climim  11877  fsumcnv  11991  fsumrelem  12025  fsumre  12026  fsumim  12027  arisum2  12053  expcnv  12058  geo2sum2  12069  geo2lim  12070  0.999...  12075  geoihalfsum  12076  fprodcnv  12179  fprodge0  12191  fprodge1  12193  ege2le3  12225  ef0  12226  reeff1  12254  tan0  12285  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  cos1bnd  12313  cos2bnd  12314  sinltxirr  12315  sin01gt0  12316  cos01gt0  12317  sin02gt0  12318  sincos1sgn  12319  sincos2sgn  12320  cos12dec  12322  egt2lt3  12334  epos  12335  ene1  12339  eap1  12340  3dvds  12418  3dvdsdec  12419  3dvds2dec  12420  odd2np1lem  12426  n2dvds1  12466  z4even  12470  ndvdsi  12487  flodddiv4  12490  bitsp1o  12507  0bits  12513  gcd0val  12524  6gcd4e2  12559  3lcm2e6woprm  12651  6lcm4e12  12652  3lcm2e6  12725  sqrt2irrlem  12726  phimullem  12790  pockthi  12924  4sqlem19  12975  dec2dvds  12977  dec5dvds2  12979  dec2nprm  12981  modxai  12982  gcdi  12986  gcdmodi  12987  numexpp1  12990  karatsuba  12996  2exp7  13000  xpnnen  13008  xpomen  13009  ennnfonelemj0  13015  ennnfonelem0  13019  ennnfonelemhf1o  13027  exmidunben  13040  qnnen  13045  unct  13056  setscom  13115  strleun  13180  prdsex  13345  prdsvallem  13348  imasival  13382  ismgm  13433  fn0g  13451  fngsum  13464  issgrp  13479  ismnddef  13494  isghm  13823  isrng  13940  rngmgpf  13943  isring  14006  mgpf  14017  dfrhm2  14161  rhmex  14164  isdomn  14276  rmodislmod  14358  lidlmex  14482  mopnset  14559  cnfldstr  14565  cnfldcj  14572  cnfld0  14578  cnfldplusf  14581  zringcrng  14599  zringmulr  14606  zringmpg  14613  znval  14643  psrval  14673  fnpsr  14674  fnmpl  14700  txtopi  14978  txunii  14981  upxp  14989  uptx  14991  cnmpt1st  15005  cnmpt2nd  15006  txswaphmeolem  15037  qtopbasss  15238  cnmet  15247  cnfldms  15253  cnopncntop  15261  cnopn  15262  remet  15265  blssioo  15270  tgqioo  15272  tgioo2cntop  15274  tgioo2  15276  divcnap  15282  abscncf  15302  recncf  15303  imcncf  15304  cjcncf  15305  mulc1cncf  15306  cncfcn1cntop  15311  idcncf  15318  cdivcncfap  15321  expcncf  15326  cnrehmeocntop  15327  maxcncf  15332  mincncf  15333  ivthreinc  15362  hovercncf  15363  limccnp2lem  15393  limccnp2cntop  15394  dvcnp2cntop  15416  dvaddxxbr  15418  dvmulxxbr  15419  dvcoapbr  15424  dvrecap  15430  dveflem  15443  dvef  15444  sincn  15486  coscn  15487  reeff1oleme  15489  reeff1o  15490  cosz12  15497  sin0pilem1  15498  sin0pilem2  15499  pipos  15505  sinhalfpilem  15508  sincosq1lem  15542  sincosq1sgn  15543  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  sinq12gt0  15547  cosq14gt0  15549  cosq23lt0  15550  coseq0q4123  15551  coseq00topi  15552  coseq0negpitopi  15553  tangtx  15555  sincos4thpi  15557  tan4thpi  15558  sincos6thpi  15559  pigt3  15561  cosordlem  15566  cosq34lt1  15567  cos02pilt1  15568  cos0pilt1  15569  ioocosf1o  15571  negpitopissre  15572  log1  15583  loge  15584  2logb9irr  15688  sqrt2cxp2logb9e3  15692  2logb9irrap  15694  mpodvdsmulf1o  15707  fsumdvdsmul  15708  1sgm2ppw  15712  lgsdir2lem2  15751  lgsdir2lem3  15752  lgseisenlem4  15795  2lgsoddprmlem3  15833  2sqlem9  15846  2sqlem10  15847  opvtxfvi  15871  opiedgfvi  15872  umgrbien  15954  usgrprc  16096  vtxdfifiun  16108  upgr2wlkdc  16186  ex-fl  16271  ex-ceil  16272  ex-bc  16275  ex-dvds  16276  ex-gcd  16277  bj-charfunbi  16356  bj-unex  16464  bj-nn0suc0  16495  bj-nntrans  16496  bj-nnelirr  16498  012of  16542  2o01f  16543  pwle2  16549  nnsf  16557  peano3nninf  16559  exmidsbthrlem  16576  sbthom  16580  isomninnlem  16584  iooref1o  16588  trilpolemisumle  16592  trilpolemeq1  16594  trilpolemlt1  16595  apdiff  16602  iswomninnlem  16603  iswomni0  16605  ismkvnnlem  16606  dceqnconst  16614  dcapnconst  16615  nconstwlpolemgt0  16618  taupi  16627