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  2805  vtocl2  2856  spc2ev  2899  sbc2ie  3100  csbieb  3166  sseq12i  3252  uneq12i  3356  ineq12i  3403  ifssun  3617  nelpri  3690  ralpr  3721  rexpr  3722  preq12i  3748  dfop  3856  opeq12i  3862  breq12i  4092  mpteq2ia  4170  exmidundif  4291  exmidundifim  4292  opex  4316  opi2  4320  opth2  4327  opeqsn  4340  opeqpr  4341  uniop  4343  opelopaba  4355  braba  4356  opelopab  4361  brab  4362  opelopabaf  4363  unex  4533  snnex  4540  op1stb  4570  ifelpwun  4575  ifex  4578  onun2i  4584  onsucssi  4599  ontriexmidim  4615  ontr2exmid  4618  onsucsssucexmid  4620  onsucelsucexmid  4623  opthreg  4649  tfis  4676  finds  4693  finds2  4694  nnregexmid  4714  xpeq12i  4742  opelvv  4771  eqrelriiv  4815  eqrelrdv  4817  xpss  4829  xpex  4837  relop  4875  brco  4896  opelcnv  4907  brcnv  4908  asymref  5117  codir  5120  ssrnres  5174  dmprop  5206  dfco2  5231  cossxp  5254  cocnvss  5257  coex  5277  funsn  5372  fnsn  5378  feq23i  5471  resasplitss  5510  fabex  5519  fvex  5652  xpsn  5816  fmptap  5836  opabex  5870  acexmidlemv  6008  oveq12i  6022  oprabid  6042  oprabss  6099  caovcom  6172  opabex3  6276  iunex  6277  oprabex  6282  ofmres  6290  op1st  6301  op2nd  6302  fo1st  6312  fo2nd  6313  mpoex  6371  1stconst  6378  2ndconst  6379  algrflem  6386  dftpos4  6420  tpostpos  6421  tpossym  6433  frecex  6551  frecfnom  6558  2oex  6590  sucinc  6604  fnoei  6611  oeiexg  6612  nnacli  6641  nnmcli  6642  elec  6734  ecovcom  6802  ecovass  6804  ecovdi  6806  fnmap  6815  mapval  6820  elmap  6837  elpm  6839  elpm2  6840  map0  6849  ixpconst  6868  entri  6951  endisj  6996  xpcomco  6998  phplem2  7027  1ndom2  7039  ssfiexmid  7051  domfiexmid  7053  exmidpw2en  7090  unfiexmid  7096  unfiin  7104  inresflem  7243  casefun  7268  caserel  7270  caseinj  7272  omp1eomlem  7277  omp1eom  7278  endjusym  7279  djufun  7287  djuinj  7289  ctssdccl  7294  ctssdclemr  7295  nninfex  7304  infnninf  7307  fodjuomnilemdc  7327  ctssexmid  7333  exmidonfinlem  7387  dju1p1e2  7391  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  exmidaclem  7406  pw1dom2  7428  onntri35  7438  onntri45  7442  2oneel  7458  2omotaplemst  7460  acnccim  7474  1lt2pi  7543  indpi  7545  1nq  7569  rec1nq  7598  1lt2nq  7609  ltaddnq  7610  halfnqq  7613  prarloclemarch2  7622  prarloclemlt  7696  prarloclemcalc  7705  genpelxp  7714  ltexprlempr  7811  recexprlempr  7835  cauappcvgprlemcl  7856  cauappcvgprlemladd  7861  caucvgprlemcl  7879  caucvgprprlemcl  7907  suplocexprlemell  7916  suplocexprlemdisj  7923  suplocexprlemub  7926  0r  7953  1sr  7954  m1r  7955  m1p1sr  7963  m1m1sr  7964  0lt1sr  7968  1ne0sr  7969  1idsr  7971  recexgt0sr  7976  prsradd  7989  caucvgsrlemoffres  8003  caucvgsr  8005  mappsrprg  8007  map2psrprg  8008  pitonnlem1p1  8049  pitonnlem2  8050  pitoregt0  8052  peano2nnnn  8056  axi2m1  8078  axprecex  8083  axcnre  8084  nnindnn  8096  nntopi  8097  0cn  8154  addcli  8166  mulcli  8167  mulcomi  8168  readdcli  8175  remulcli  8176  rexpssxrxp  8207  ltrelxr  8223  gtneii  8258  lttri3i  8260  letri3i  8261  ltnsymi  8262  lenlti  8263  ltlei  8264  mulgt0i  8272  mulgt0ii  8273  0lt1  8289  addcomi  8306  pncan3oi  8378  resubcli  8425  subcli  8438  pncan3i  8439  negsubi  8440  subnegi  8441  subeq0i  8442  neg11i  8443  negcon1i  8444  negcon2i  8445  mulneg1i  8566  mulneg2i  8567  mul2negi  8568  addgt0ii  8654  ltnegi  8656  lenegi  8657  ltnegcon2i  8658  lesub0i  8659  ltaddposi  8660  posdifi  8661  ltnegcon1i  8662  lenegcon1i  8663  subge0i  8664  1ap0  8753  ltapii  8798  recrecapi  8907  dividapi  8908  div0api  8909  rec11apii  8924  divdiv32api  8930  recgt0ii  9070  ltrecii  9081  ltdiv23ii  9090  sup3exmid  9120  nnssre  9130  nnind  9142  nnmulcli  9148  nnsubi  9166  0le2  9216  1lt3  9298  2lt4  9300  1lt4  9301  3lt5  9303  2lt5  9304  1lt5  9305  4lt6  9307  3lt6  9308  2lt6  9309  1lt6  9310  5lt7  9312  4lt7  9313  3lt7  9314  2lt7  9315  1lt7  9316  6lt8  9318  5lt8  9319  4lt8  9320  3lt8  9321  2lt8  9322  1lt8  9323  7lt9  9325  6lt9  9326  5lt9  9327  4lt9  9328  3lt9  9329  2lt9  9330  1lt9  9331  2muline0  9352  nn0addcli  9422  nn0mulcli  9423  nn0addge1i  9433  nn0addge2i  9434  dfz2  9535  halfnz  9559  9p1e10  9596  numnncl  9603  numltc  9619  le9lt10  9620  nummac  9638  8lt10  9725  7lt10  9726  6lt10  9727  5lt10  9728  4lt10  9729  3lt10  9730  2lt10  9731  1lt10  9732  eluzaddi  9766  eluzsubi  9767  eluz2nn  9778  eluz4eluz2  9779  uzuzle23  9783  eluzge3nn  9784  divfnzn  9833  elq  9834  qreccl  9854  xrltnr  9992  mnfltpnf  9998  xaddmnf1  10061  pnfaddmnf  10063  mnfaddpnf  10064  xrex  10069  xaddid1  10075  xsubge0  10094  xposdif  10095  xleaddadd  10100  elicc2i  10152  ioomax  10161  iccmax  10162  ioopos  10163  elxrge0  10191  iccshftri  10208  iccshftli  10210  iccdili  10212  icccntri  10214  unitssre  10218  fz10  10259  fzpreddisj  10284  fz0to4untppr  10337  dfrp2  10500  fldiv4p1lem1div2  10542  fldiv4lem1div2  10544  frecfzennn  10665  xnn0nnen  10676  fnn0nninf  10677  fxnn0nninf  10678  0tonninf  10679  1tonninf  10680  m1expcl2  10800  m1expcl  10801  nn0expcli  10804  sqmuli  10861  cu2  10877  i3  10880  subsqi  10888  binom2subi  10894  bcpasc  11005  4bc2eq6  11013  hashinfom  11017  prhash2ex  11049  hashp1i  11050  lsw0g  11138  swrdccat3blem  11292  rei  11431  imi  11432  readdi  11460  imaddi  11461  remuli  11462  immuli  11463  cjaddi  11464  cjmuli  11465  ipcni  11466  crrei  11468  crimi  11469  rexfiuz  11521  sqrt1  11578  sqrt4  11579  sqrt9  11580  abs1  11604  sqrtmulii  11666  abslti  11670  abslei  11671  abssubi  11682  absmuli  11683  sqabsaddi  11684  sqabssubi  11685  abstrii  11687  fimaxre2  11759  climz  11824  abscn2  11847  recn2  11849  imcn2  11850  climabs  11852  climre  11854  climim  11855  fsumcnv  11969  fsumrelem  12003  fsumre  12004  fsumim  12005  arisum2  12031  expcnv  12036  geo2sum2  12047  geo2lim  12048  0.999...  12053  geoihalfsum  12054  fprodcnv  12157  fprodge0  12169  fprodge1  12171  ege2le3  12203  ef0  12204  reeff1  12232  tan0  12263  ef01bndlem  12288  sin01bnd  12289  cos01bnd  12290  cos1bnd  12291  cos2bnd  12292  sinltxirr  12293  sin01gt0  12294  cos01gt0  12295  sin02gt0  12296  sincos1sgn  12297  sincos2sgn  12298  cos12dec  12300  egt2lt3  12312  epos  12313  ene1  12317  eap1  12318  3dvds  12396  3dvdsdec  12397  3dvds2dec  12398  odd2np1lem  12404  n2dvds1  12444  z4even  12448  ndvdsi  12465  flodddiv4  12468  bitsp1o  12485  0bits  12491  gcd0val  12502  6gcd4e2  12537  3lcm2e6woprm  12629  6lcm4e12  12630  3lcm2e6  12703  sqrt2irrlem  12704  phimullem  12768  pockthi  12902  4sqlem19  12953  dec2dvds  12955  dec5dvds2  12957  dec2nprm  12959  modxai  12960  gcdi  12964  gcdmodi  12965  numexpp1  12968  karatsuba  12974  2exp7  12978  xpnnen  12986  xpomen  12987  ennnfonelemj0  12993  ennnfonelem0  12997  ennnfonelemhf1o  13005  exmidunben  13018  qnnen  13023  unct  13034  setscom  13093  strleun  13158  prdsex  13323  prdsvallem  13326  imasival  13360  ismgm  13411  fn0g  13429  fngsum  13442  issgrp  13457  ismnddef  13472  isghm  13801  isrng  13918  rngmgpf  13921  isring  13984  mgpf  13995  dfrhm2  14139  rhmex  14142  isdomn  14254  rmodislmod  14336  lidlmex  14460  mopnset  14537  cnfldstr  14543  cnfldcj  14550  cnfld0  14556  cnfldplusf  14559  zringcrng  14577  zringmulr  14584  zringmpg  14591  znval  14621  psrval  14651  fnpsr  14652  fnmpl  14678  txtopi  14956  txunii  14959  upxp  14967  uptx  14969  cnmpt1st  14983  cnmpt2nd  14984  txswaphmeolem  15015  qtopbasss  15216  cnmet  15225  cnfldms  15231  cnopncntop  15239  cnopn  15240  remet  15243  blssioo  15248  tgqioo  15250  tgioo2cntop  15252  tgioo2  15254  divcnap  15260  abscncf  15280  recncf  15281  imcncf  15282  cjcncf  15283  mulc1cncf  15284  cncfcn1cntop  15289  idcncf  15296  cdivcncfap  15299  expcncf  15304  cnrehmeocntop  15305  maxcncf  15310  mincncf  15311  ivthreinc  15340  hovercncf  15341  limccnp2lem  15371  limccnp2cntop  15372  dvcnp2cntop  15394  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvrecap  15408  dveflem  15421  dvef  15422  sincn  15464  coscn  15465  reeff1oleme  15467  reeff1o  15468  cosz12  15475  sin0pilem1  15476  sin0pilem2  15477  pipos  15483  sinhalfpilem  15486  sincosq1lem  15520  sincosq1sgn  15521  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  sinq12gt0  15525  cosq14gt0  15527  cosq23lt0  15528  coseq0q4123  15529  coseq00topi  15530  coseq0negpitopi  15531  tangtx  15533  sincos4thpi  15535  tan4thpi  15536  sincos6thpi  15537  pigt3  15539  cosordlem  15544  cosq34lt1  15545  cos02pilt1  15546  cos0pilt1  15547  ioocosf1o  15549  negpitopissre  15550  log1  15561  loge  15562  2logb9irr  15666  sqrt2cxp2logb9e3  15670  2logb9irrap  15672  mpodvdsmulf1o  15685  fsumdvdsmul  15686  1sgm2ppw  15690  lgsdir2lem2  15729  lgsdir2lem3  15730  lgseisenlem4  15773  2lgsoddprmlem3  15811  2sqlem9  15824  2sqlem10  15825  opvtxfvi  15849  opiedgfvi  15850  umgrbien  15931  usgrprc  16071  vtxdfifiun  16083  upgr2wlkdc  16147  ex-fl  16198  ex-ceil  16199  ex-bc  16202  ex-dvds  16203  ex-gcd  16204  bj-charfunbi  16283  bj-unex  16391  bj-nn0suc0  16422  bj-nntrans  16423  bj-nnelirr  16425  012of  16470  2o01f  16471  pwle2  16477  nnsf  16485  peano3nninf  16487  exmidsbthrlem  16504  sbthom  16508  isomninnlem  16512  iooref1o  16516  trilpolemisumle  16520  trilpolemeq1  16522  trilpolemlt1  16523  apdiff  16530  iswomninnlem  16531  iswomni0  16533  ismkvnnlem  16534  dceqnconst  16542  dcapnconst  16543  nconstwlpolemgt0  16546  taupi  16555