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  2179  eqeq12i  2246  el2v  2818  vtocl2  2869  spc2ev  2912  sbc2ie  3113  csbieb  3179  sseq12i  3265  uneq12i  3370  ineq12i  3419  ifssun  3636  nelpri  3712  ralpr  3743  rexpr  3744  preq12i  3772  dfop  3881  opeq12i  3887  breq12i  4117  mpteq2ia  4195  exmidundif  4318  exmidundifim  4319  opex  4344  opi2  4348  opth2  4355  opeqsn  4368  opeqpr  4369  uniop  4371  opelopaba  4383  braba  4384  opelopab  4389  brab  4390  opelopabaf  4391  unex  4561  snnex  4568  op1stb  4598  ifelpwun  4603  ifex  4606  onun2i  4612  onsucssi  4627  ontriexmidim  4643  ontr2exmid  4646  onsucsssucexmid  4648  onsucelsucexmid  4651  opthreg  4677  tfis  4704  finds  4721  finds2  4722  nnregexmid  4742  xpeq12i  4770  opelvv  4799  eqrelriiv  4843  eqrelrdv  4845  xpss  4857  xpex  4865  relop  4904  brco  4925  opelcnv  4936  brcnv  4937  asymref  5147  codir  5150  ssrnres  5204  dmprop  5236  dfco2  5261  cossxp  5284  cocnvss  5287  coex  5307  funsn  5403  fnsn  5409  feq23i  5502  resasplitss  5543  fabex  5554  fvex  5689  xpsn  5853  fmptap  5873  opabex  5909  acexmidlemv  6047  oveq12i  6061  oprabid  6081  oprabss  6138  caovcom  6211  opabex3  6314  iunex  6315  oprabex  6320  ofmres  6328  op1st  6339  op2nd  6340  fo1st  6350  fo2nd  6351  mpoex  6409  1stconst  6416  2ndconst  6417  algrflem  6424  dftpos4  6493  tpostpos  6494  tpossym  6506  frecex  6624  frecfnom  6631  2oex  6663  sucinc  6677  fnoei  6684  oeiexg  6685  nnacli  6714  nnmcli  6715  elec  6807  ecovcom  6875  ecovass  6877  ecovdi  6879  fnmap  6888  mapval  6893  elmap  6910  elpm  6912  elpm2  6913  map0  6923  ixpconst  6942  entri  7025  endisj  7074  xpcomco  7076  phplem2  7106  1ndom2  7118  ssfiexmid  7130  domfiexmid  7134  exmidpw2en  7171  unfiexmid  7177  unfiin  7185  inresflem  7350  casefun  7375  caserel  7377  caseinj  7379  omp1eomlem  7384  omp1eom  7385  endjusym  7386  djufun  7394  djuinj  7396  ctssdccl  7401  ctssdclemr  7402  nninfex  7411  infnninf  7414  fodjuomnilemdc  7434  ctssexmid  7440  exmidonfinlem  7495  dju1p1e2  7499  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  exmidaclem  7514  pw1dom2  7536  onntri35  7546  onntri45  7550  2oneel  7566  2omotaplemst  7568  acnccim  7582  1lt2pi  7651  indpi  7653  1nq  7677  rec1nq  7706  1lt2nq  7717  ltaddnq  7718  halfnqq  7721  prarloclemarch2  7730  prarloclemlt  7804  prarloclemcalc  7813  genpelxp  7822  ltexprlempr  7919  recexprlempr  7943  cauappcvgprlemcl  7964  cauappcvgprlemladd  7969  caucvgprlemcl  7987  caucvgprprlemcl  8015  suplocexprlemell  8024  suplocexprlemdisj  8031  suplocexprlemub  8034  0r  8061  1sr  8062  m1r  8063  m1p1sr  8071  m1m1sr  8072  0lt1sr  8076  1ne0sr  8077  1idsr  8079  recexgt0sr  8084  prsradd  8097  caucvgsrlemoffres  8111  caucvgsr  8113  mappsrprg  8115  map2psrprg  8116  pitonnlem1p1  8157  pitonnlem2  8158  pitoregt0  8160  peano2nnnn  8164  axi2m1  8186  axprecex  8191  axcnre  8192  nnindnn  8204  nntopi  8205  0cn  8262  addcli  8274  mulcli  8275  mulcomi  8276  readdcli  8283  remulcli  8284  rexpssxrxp  8314  ltrelxr  8330  gtneii  8365  lttri3i  8367  letri3i  8368  ltnsymi  8369  lenlti  8370  ltlei  8371  mulgt0i  8379  mulgt0ii  8380  0lt1  8396  addcomi  8413  pncan3oi  8485  resubcli  8532  subcli  8545  pncan3i  8546  negsubi  8547  subnegi  8548  subeq0i  8549  neg11i  8550  negcon1i  8551  negcon2i  8552  mulneg1i  8673  mulneg2i  8674  mul2negi  8675  addgt0ii  8761  ltnegi  8763  lenegi  8764  ltnegcon2i  8765  lesub0i  8766  ltaddposi  8767  posdifi  8768  ltnegcon1i  8769  lenegcon1i  8770  subge0i  8771  1ap0  8860  ltapii  8905  recrecapi  9014  dividapi  9015  div0api  9016  rec11apii  9031  divdiv32api  9037  recgt0ii  9177  ltrecii  9188  ltdiv23ii  9197  sup3exmid  9227  nnssre  9237  nnind  9249  nnmulcli  9255  nnsubi  9273  0le2  9323  1lt3  9405  2lt4  9407  1lt4  9408  3lt5  9410  2lt5  9411  1lt5  9412  4lt6  9414  3lt6  9415  2lt6  9416  1lt6  9417  5lt7  9419  4lt7  9420  3lt7  9421  2lt7  9422  1lt7  9423  6lt8  9425  5lt8  9426  4lt8  9427  3lt8  9428  2lt8  9429  1lt8  9430  7lt9  9432  6lt9  9433  5lt9  9434  4lt9  9435  3lt9  9436  2lt9  9437  1lt9  9438  2muline0  9459  nn0addcli  9529  nn0mulcli  9530  nn0addge1i  9540  nn0addge2i  9541  dfz2  9646  halfnz  9670  9p1e10  9707  numnncl  9714  numltc  9730  le9lt10  9731  nummac  9749  8lt10  9836  7lt10  9837  6lt10  9838  5lt10  9839  4lt10  9840  3lt10  9841  2lt10  9842  1lt10  9843  eluzaddi  9877  eluzsubi  9878  uzuzle23  9890  uzuzle24  9891  uzuzle34  9892  eluz2nn  9894  eluz4eluz2  9896  eluzge3nn  9900  divfnzn  9949  elq  9950  qreccl  9970  xrltnr  10108  mnfltpnf  10114  xaddmnf1  10177  pnfaddmnf  10179  mnfaddpnf  10180  xrex  10185  xaddid1  10191  xsubge0  10210  xposdif  10211  xleaddadd  10216  elicc2i  10268  ioomax  10277  iccmax  10278  ioopos  10279  elxrge0  10307  iccshftri  10324  iccshftli  10326  iccdili  10328  icccntri  10330  unitssre  10335  fz10  10376  fzpreddisj  10401  fz0to4untppr  10454  dfrp2  10619  fldiv4p1lem1div2  10661  fldiv4lem1div2  10663  frecfzennn  10784  xnn0nnen  10795  fnn0nninf  10796  fxnn0nninf  10797  0tonninf  10798  1tonninf  10799  m1expcl2  10919  m1expcl  10920  nn0expcli  10923  sqmuli  10980  cu2  10996  i3  10999  subsqi  11007  binom2subi  11013  bcpasc  11124  4bc2eq6  11132  hashinfom  11136  prhash2ex  11169  hashp1i  11170  lsw0g  11266  swrdccat3blem  11424  rei  11577  imi  11578  readdi  11606  imaddi  11607  remuli  11608  immuli  11609  cjaddi  11610  cjmuli  11611  ipcni  11612  crrei  11614  crimi  11615  rexfiuz  11667  sqrt1  11724  sqrt4  11725  sqrt9  11726  abs1  11750  sqrtmulii  11812  abslti  11816  abslei  11817  abssubi  11828  absmuli  11829  sqabsaddi  11830  sqabssubi  11831  abstrii  11833  fimaxre2  11905  climz  11970  abscn2  11993  recn2  11995  imcn2  11996  climabs  11998  climre  12000  climim  12001  fsumcnv  12116  fsumrelem  12150  fsumre  12151  fsumim  12152  arisum2  12178  expcnv  12183  geo2sum2  12194  geo2lim  12195  0.999...  12200  geoihalfsum  12201  fprodcnv  12304  fprodge0  12316  fprodge1  12318  ege2le3  12350  ef0  12351  reeff1  12379  tan0  12410  ef01bndlem  12435  sin01bnd  12436  cos01bnd  12437  cos1bnd  12438  cos2bnd  12439  sinltxirr  12440  sin01gt0  12441  cos01gt0  12442  sin02gt0  12443  sincos1sgn  12444  sincos2sgn  12445  cos12dec  12447  egt2lt3  12459  epos  12460  ene1  12464  eap1  12465  3dvds  12543  3dvdsdec  12544  3dvds2dec  12545  odd2np1lem  12551  n2dvds1  12591  z4even  12595  ndvdsi  12612  flodddiv4  12615  bitsp1o  12632  0bits  12638  gcd0val  12649  6gcd4e2  12684  3lcm2e6woprm  12776  6lcm4e12  12777  3lcm2e6  12850  sqrt2irrlem  12851  phimullem  12915  pockthi  13049  4sqlem19  13100  dec2dvds  13102  dec5dvds2  13104  dec2nprm  13106  modxai  13107  gcdi  13111  gcdmodi  13112  numexpp1  13115  karatsuba  13121  2exp7  13125  ballotfilemofi  13131  xpnnen  13134  xpomen  13135  ennnfonelemj0  13141  ennnfonelem0  13145  ennnfonelemhf1o  13153  exmidunben  13166  qnnen  13171  unct  13182  setscom  13241  strleun  13306  prdsex  13471  prdsvallem  13474  imasival  13508  ismgm  13559  fn0g  13577  fngsum  13590  issgrp  13605  ismnddef  13620  isghm  13949  isrng  14067  rngmgpf  14070  isring  14133  mgpf  14144  dfrhm2  14288  rhmex  14291  isdomn  14404  rmodislmod  14486  lidlmex  14610  mopnset  14687  cnfldstr  14693  cnfldcj  14700  cnfld0  14706  cnfldplusf  14709  zringcrng  14727  zringmulr  14734  zringmpg  14741  znval  14771  psrval  14801  fnpsr  14802  fnmpl  14835  txtopi  15113  txunii  15116  upxp  15124  uptx  15126  cnmpt1st  15140  cnmpt2nd  15141  txswaphmeolem  15172  qtopbasss  15373  cnmet  15382  cnfldms  15388  cnopncntop  15396  cnopn  15397  remet  15400  blssioo  15405  tgqioo  15407  tgioo2cntop  15409  tgioo2  15411  divcnap  15417  abscncf  15437  recncf  15438  imcncf  15439  cjcncf  15440  mulc1cncf  15441  cncfcn1cntop  15446  idcncf  15453  cdivcncfap  15456  expcncf  15461  cnrehmeocntop  15462  maxcncf  15467  mincncf  15468  ivthreinc  15497  hovercncf  15498  limccnp2lem  15528  limccnp2cntop  15529  dvcnp2cntop  15551  dvaddxxbr  15553  dvmulxxbr  15554  dvcoapbr  15559  dvrecap  15565  dveflem  15578  dvef  15579  sincn  15621  coscn  15622  reeff1oleme  15624  reeff1o  15625  cosz12  15632  sin0pilem1  15633  sin0pilem2  15634  pipos  15640  sinhalfpilem  15643  sincosq1lem  15677  sincosq1sgn  15678  sincosq2sgn  15679  sincosq3sgn  15680  sincosq4sgn  15681  sinq12gt0  15682  cosq14gt0  15684  cosq23lt0  15685  coseq0q4123  15686  coseq00topi  15687  coseq0negpitopi  15688  tangtx  15690  sincos4thpi  15692  tan4thpi  15693  sincos6thpi  15694  pigt3  15696  cosordlem  15701  cosq34lt1  15702  cos02pilt1  15703  cos0pilt1  15704  ioocosf1o  15706  negpitopissre  15707  log1  15718  loge  15719  2logb9irr  15823  sqrt2cxp2logb9e3  15827  2logb9irrap  15829  mpodvdsmulf1o  15845  fsumdvdsmul  15846  1sgm2ppw  15850  lgsdir2lem2  15889  lgsdir2lem3  15890  lgseisenlem4  15933  2lgsoddprmlem3  15971  2sqlem9  15984  2sqlem10  15985  opvtxfvi  16009  opiedgfvi  16010  umgrbien  16092  usgrprc  16234  vtxdfifiun  16279  upgr2wlkdc  16359  konigsbergvtx  16464  konigsbergiedg  16465  konigsbergumgr  16469  konigsberglem1  16470  konigsberglem2  16471  konigsberglem3  16472  konigsberglem5  16474  konigsberg  16475  ex-fl  16480  ex-ceil  16481  ex-bc  16484  ex-dvds  16485  ex-gcd  16486  bj-charfunbi  16568  bj-unex  16676  bj-nn0suc0  16707  bj-nntrans  16708  bj-nnelirr  16710  012of  16754  2o01f  16755  pwle2  16759  nnsf  16770  peano3nninf  16772  exmidsbthrlem  16789  sbthom  16793  repiecelem  16796  repiecele0  16797  repiecege0  16798  isomninnlem  16801  iooref1o  16805  trilpolemisumle  16809  trilpolemeq1  16811  trilpolemlt1  16812  apdiff  16819  iswomninnlem  16821  iswomni0  16823  ismkvnnlem  16824  dceqnconst  16832  dcapnconst  16833  nconstwlpolemgt0  16836  taupi  16845