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  2178  eqeq12i  2245  el2v  2808  vtocl2  2859  spc2ev  2902  sbc2ie  3103  csbieb  3169  sseq12i  3255  uneq12i  3359  ineq12i  3406  ifssun  3620  nelpri  3693  ralpr  3724  rexpr  3725  preq12i  3753  dfop  3861  opeq12i  3867  breq12i  4097  mpteq2ia  4175  exmidundif  4296  exmidundifim  4297  opex  4321  opi2  4325  opth2  4332  opeqsn  4345  opeqpr  4346  uniop  4348  opelopaba  4360  braba  4361  opelopab  4366  brab  4367  opelopabaf  4368  unex  4538  snnex  4545  op1stb  4575  ifelpwun  4580  ifex  4583  onun2i  4589  onsucssi  4604  ontriexmidim  4620  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  opthreg  4654  tfis  4681  finds  4698  finds2  4699  nnregexmid  4719  xpeq12i  4747  opelvv  4776  eqrelriiv  4820  eqrelrdv  4822  xpss  4834  xpex  4842  relop  4880  brco  4901  opelcnv  4912  brcnv  4913  asymref  5122  codir  5125  ssrnres  5179  dmprop  5211  dfco2  5236  cossxp  5259  cocnvss  5262  coex  5282  funsn  5378  fnsn  5384  feq23i  5477  resasplitss  5516  fabex  5525  fvex  5659  xpsn  5824  fmptap  5844  opabex  5878  acexmidlemv  6016  oveq12i  6030  oprabid  6050  oprabss  6107  caovcom  6180  opabex3  6284  iunex  6285  oprabex  6290  ofmres  6298  op1st  6309  op2nd  6310  fo1st  6320  fo2nd  6321  mpoex  6379  1stconst  6386  2ndconst  6387  algrflem  6394  dftpos4  6429  tpostpos  6430  tpossym  6442  frecex  6560  frecfnom  6567  2oex  6599  sucinc  6613  fnoei  6620  oeiexg  6621  nnacli  6650  nnmcli  6651  elec  6743  ecovcom  6811  ecovass  6813  ecovdi  6815  fnmap  6824  mapval  6829  elmap  6846  elpm  6848  elpm2  6849  map0  6858  ixpconst  6877  entri  6960  endisj  7008  xpcomco  7010  phplem2  7039  1ndom2  7051  ssfiexmid  7063  domfiexmid  7067  exmidpw2en  7104  unfiexmid  7110  unfiin  7118  inresflem  7259  casefun  7284  caserel  7286  caseinj  7288  omp1eomlem  7293  omp1eom  7294  endjusym  7295  djufun  7303  djuinj  7305  ctssdccl  7310  ctssdclemr  7311  nninfex  7320  infnninf  7323  fodjuomnilemdc  7343  ctssexmid  7349  exmidonfinlem  7404  dju1p1e2  7408  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  pw1dom2  7445  onntri35  7455  onntri45  7459  2oneel  7475  2omotaplemst  7477  acnccim  7491  1lt2pi  7560  indpi  7562  1nq  7586  rec1nq  7615  1lt2nq  7626  ltaddnq  7627  halfnqq  7630  prarloclemarch2  7639  prarloclemlt  7713  prarloclemcalc  7722  genpelxp  7731  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  cauappcvgprlemladd  7878  caucvgprlemcl  7896  caucvgprprlemcl  7924  suplocexprlemell  7933  suplocexprlemdisj  7940  suplocexprlemub  7943  0r  7970  1sr  7971  m1r  7972  m1p1sr  7980  m1m1sr  7981  0lt1sr  7985  1ne0sr  7986  1idsr  7988  recexgt0sr  7993  prsradd  8006  caucvgsrlemoffres  8020  caucvgsr  8022  mappsrprg  8024  map2psrprg  8025  pitonnlem1p1  8066  pitonnlem2  8067  pitoregt0  8069  peano2nnnn  8073  axi2m1  8095  axprecex  8100  axcnre  8101  nnindnn  8113  nntopi  8114  0cn  8171  addcli  8183  mulcli  8184  mulcomi  8185  readdcli  8192  remulcli  8193  rexpssxrxp  8224  ltrelxr  8240  gtneii  8275  lttri3i  8277  letri3i  8278  ltnsymi  8279  lenlti  8280  ltlei  8281  mulgt0i  8289  mulgt0ii  8290  0lt1  8306  addcomi  8323  pncan3oi  8395  resubcli  8442  subcli  8455  pncan3i  8456  negsubi  8457  subnegi  8458  subeq0i  8459  neg11i  8460  negcon1i  8461  negcon2i  8462  mulneg1i  8583  mulneg2i  8584  mul2negi  8585  addgt0ii  8671  ltnegi  8673  lenegi  8674  ltnegcon2i  8675  lesub0i  8676  ltaddposi  8677  posdifi  8678  ltnegcon1i  8679  lenegcon1i  8680  subge0i  8681  1ap0  8770  ltapii  8815  recrecapi  8924  dividapi  8925  div0api  8926  rec11apii  8941  divdiv32api  8947  recgt0ii  9087  ltrecii  9098  ltdiv23ii  9107  sup3exmid  9137  nnssre  9147  nnind  9159  nnmulcli  9165  nnsubi  9183  0le2  9233  1lt3  9315  2lt4  9317  1lt4  9318  3lt5  9320  2lt5  9321  1lt5  9322  4lt6  9324  3lt6  9325  2lt6  9326  1lt6  9327  5lt7  9329  4lt7  9330  3lt7  9331  2lt7  9332  1lt7  9333  6lt8  9335  5lt8  9336  4lt8  9337  3lt8  9338  2lt8  9339  1lt8  9340  7lt9  9342  6lt9  9343  5lt9  9344  4lt9  9345  3lt9  9346  2lt9  9347  1lt9  9348  2muline0  9369  nn0addcli  9439  nn0mulcli  9440  nn0addge1i  9450  nn0addge2i  9451  dfz2  9552  halfnz  9576  9p1e10  9613  numnncl  9620  numltc  9636  le9lt10  9637  nummac  9655  8lt10  9742  7lt10  9743  6lt10  9744  5lt10  9745  4lt10  9746  3lt10  9747  2lt10  9748  1lt10  9749  eluzaddi  9783  eluzsubi  9784  uzuzle23  9796  uzuzle24  9797  uzuzle34  9798  eluz2nn  9800  eluz4eluz2  9802  eluzge3nn  9806  divfnzn  9855  elq  9856  qreccl  9876  xrltnr  10014  mnfltpnf  10020  xaddmnf1  10083  pnfaddmnf  10085  mnfaddpnf  10086  xrex  10091  xaddid1  10097  xsubge0  10116  xposdif  10117  xleaddadd  10122  elicc2i  10174  ioomax  10183  iccmax  10184  ioopos  10185  elxrge0  10213  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  unitssre  10240  fz10  10281  fzpreddisj  10306  fz0to4untppr  10359  dfrp2  10523  fldiv4p1lem1div2  10565  fldiv4lem1div2  10567  frecfzennn  10688  xnn0nnen  10699  fnn0nninf  10700  fxnn0nninf  10701  0tonninf  10702  1tonninf  10703  m1expcl2  10823  m1expcl  10824  nn0expcli  10827  sqmuli  10884  cu2  10900  i3  10903  subsqi  10911  binom2subi  10917  bcpasc  11028  4bc2eq6  11036  hashinfom  11040  prhash2ex  11073  hashp1i  11074  lsw0g  11162  swrdccat3blem  11320  rei  11460  imi  11461  readdi  11489  imaddi  11490  remuli  11491  immuli  11492  cjaddi  11493  cjmuli  11494  ipcni  11495  crrei  11497  crimi  11498  rexfiuz  11550  sqrt1  11607  sqrt4  11608  sqrt9  11609  abs1  11633  sqrtmulii  11695  abslti  11699  abslei  11700  abssubi  11711  absmuli  11712  sqabsaddi  11713  sqabssubi  11714  abstrii  11716  fimaxre2  11788  climz  11853  abscn2  11876  recn2  11878  imcn2  11879  climabs  11881  climre  11883  climim  11884  fsumcnv  11999  fsumrelem  12033  fsumre  12034  fsumim  12035  arisum2  12061  expcnv  12066  geo2sum2  12077  geo2lim  12078  0.999...  12083  geoihalfsum  12084  fprodcnv  12187  fprodge0  12199  fprodge1  12201  ege2le3  12233  ef0  12234  reeff1  12262  tan0  12293  ef01bndlem  12318  sin01bnd  12319  cos01bnd  12320  cos1bnd  12321  cos2bnd  12322  sinltxirr  12323  sin01gt0  12324  cos01gt0  12325  sin02gt0  12326  sincos1sgn  12327  sincos2sgn  12328  cos12dec  12330  egt2lt3  12342  epos  12343  ene1  12347  eap1  12348  3dvds  12426  3dvdsdec  12427  3dvds2dec  12428  odd2np1lem  12434  n2dvds1  12474  z4even  12478  ndvdsi  12495  flodddiv4  12498  bitsp1o  12515  0bits  12521  gcd0val  12532  6gcd4e2  12567  3lcm2e6woprm  12659  6lcm4e12  12660  3lcm2e6  12733  sqrt2irrlem  12734  phimullem  12798  pockthi  12932  4sqlem19  12983  dec2dvds  12985  dec5dvds2  12987  dec2nprm  12989  modxai  12990  gcdi  12994  gcdmodi  12995  numexpp1  12998  karatsuba  13004  2exp7  13008  xpnnen  13016  xpomen  13017  ennnfonelemj0  13023  ennnfonelem0  13027  ennnfonelemhf1o  13035  exmidunben  13048  qnnen  13053  unct  13064  setscom  13123  strleun  13188  prdsex  13353  prdsvallem  13356  imasival  13390  ismgm  13441  fn0g  13459  fngsum  13472  issgrp  13487  ismnddef  13502  isghm  13831  isrng  13949  rngmgpf  13952  isring  14015  mgpf  14026  dfrhm2  14170  rhmex  14173  isdomn  14285  rmodislmod  14367  lidlmex  14491  mopnset  14568  cnfldstr  14574  cnfldcj  14581  cnfld0  14587  cnfldplusf  14590  zringcrng  14608  zringmulr  14615  zringmpg  14622  znval  14652  psrval  14682  fnpsr  14683  fnmpl  14709  txtopi  14987  txunii  14990  upxp  14998  uptx  15000  cnmpt1st  15014  cnmpt2nd  15015  txswaphmeolem  15046  qtopbasss  15247  cnmet  15256  cnfldms  15262  cnopncntop  15270  cnopn  15271  remet  15274  blssioo  15279  tgqioo  15281  tgioo2cntop  15283  tgioo2  15285  divcnap  15291  abscncf  15311  recncf  15312  imcncf  15313  cjcncf  15314  mulc1cncf  15315  cncfcn1cntop  15320  idcncf  15327  cdivcncfap  15330  expcncf  15335  cnrehmeocntop  15336  maxcncf  15341  mincncf  15342  ivthreinc  15371  hovercncf  15372  limccnp2lem  15402  limccnp2cntop  15403  dvcnp2cntop  15425  dvaddxxbr  15427  dvmulxxbr  15428  dvcoapbr  15433  dvrecap  15439  dveflem  15452  dvef  15453  sincn  15495  coscn  15496  reeff1oleme  15498  reeff1o  15499  cosz12  15506  sin0pilem1  15507  sin0pilem2  15508  pipos  15514  sinhalfpilem  15517  sincosq1lem  15551  sincosq1sgn  15552  sincosq2sgn  15553  sincosq3sgn  15554  sincosq4sgn  15555  sinq12gt0  15556  cosq14gt0  15558  cosq23lt0  15559  coseq0q4123  15560  coseq00topi  15561  coseq0negpitopi  15562  tangtx  15564  sincos4thpi  15566  tan4thpi  15567  sincos6thpi  15568  pigt3  15570  cosordlem  15575  cosq34lt1  15576  cos02pilt1  15577  cos0pilt1  15578  ioocosf1o  15580  negpitopissre  15581  log1  15592  loge  15593  2logb9irr  15697  sqrt2cxp2logb9e3  15701  2logb9irrap  15703  mpodvdsmulf1o  15716  fsumdvdsmul  15717  1sgm2ppw  15721  lgsdir2lem2  15760  lgsdir2lem3  15761  lgseisenlem4  15804  2lgsoddprmlem3  15842  2sqlem9  15855  2sqlem10  15856  opvtxfvi  15880  opiedgfvi  15881  umgrbien  15963  usgrprc  16105  vtxdfifiun  16150  upgr2wlkdc  16230  ex-fl  16324  ex-ceil  16325  ex-bc  16328  ex-dvds  16329  ex-gcd  16330  bj-charfunbi  16409  bj-unex  16517  bj-nn0suc0  16548  bj-nntrans  16549  bj-nnelirr  16551  012of  16595  2o01f  16596  pwle2  16602  nnsf  16610  peano3nninf  16612  exmidsbthrlem  16629  sbthom  16633  isomninnlem  16637  iooref1o  16641  trilpolemisumle  16645  trilpolemeq1  16647  trilpolemlt1  16648  apdiff  16655  iswomninnlem  16656  iswomni0  16658  ismkvnnlem  16659  dceqnconst  16667  dcapnconst  16668  nconstwlpolemgt0  16671  taupi  16680