Axiom ax-mp 6

Description: Rule of Modus Ponens. The postulated inference rule of propositional calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if φ is true, and φ implies ψ, then ψ must also be true." This rule is sometimes called "detachment", since it detaches the minor premise from the major premise.

Hypotheses

Ref	Expression
min	⊢ φ
maj	⊢ (φ → ψ)

Assertion

Ref	Expression
ax-mp	⊢ ψ

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff ψ

This axiom is referenced by:  a1i 7  a2i 8  id 9  id1 10  syl 12  syl4 19  syld 27  mp2 43  mpi 44  mpd 46  pm2.43i 58  pm2.86i 64  a3i 69  mto 93  mt2 96  mt3 99  pm2.65i 116  impi 124  expi 125  biigb 129  bi1 130  bi2 131  bi3 132  biimp 133  biimpr 134  mpbi 164  mpbir 165  a1bi 172  anc2li 250  anc2ri 251  pm3.26i 257  pm3.27i 261  mpan 518  mp2an 520  biantru 543  biantrur 544  biorfi 552  3jaoi 633  merlem1 645  merlem2 646  merlem3 647  merlem4 648  merlem5 649  merlem6 650  merlem7 651  merlem8 652  merlem9 653  merlem10 654  merlem11 655  merlem12 656  merlem13 657  luk-1 658  luk-2 659  luk-3 660  luklem1 661  luklem2 662  luklem4 664  luklem6 666  luklem7 667  luklem8 668  ax2 670  a4i 680  mpg 684  exan 784  eqvin.l1 851  sbid 868  sbie 904  sbco 910  a4w1 930  bieu 1014  bimo 1031  eumoi 1038  moani 1047  zfext2 1087  cleq1i 1108  cleq2i 1111  eleq1i 1152  eleq2i 1153  biral 1223  birex 1224  rspec 1246  mprg 1249  elisseti 1355  ceqsal 1363  vtoclf 1377  vtocle 1391  vtoclef 1392  cla4v 1400  elab2 1419  euxfr 1436  sbc5 1452  zfaus 1480  bm1.3ii 1481  nalset 1482  sseli 1504  sselii 1505  sseq1i 1524  sseq2i 1525  psseq1i 1561  psseq2i 1562  difeq1i 1584  difeq2i 1585  uneq1i 1607  uneq2i 1608  ineq1i 1641  ineq2i 1642  ssinss1 1664  ssexi 1701  rabex 1706  zfnul 1746  0dif 1757  sneqi 1817  elpr 1823  elsnc 1826  elsnc2 1832  pri1 1841  tpi1 1843  tpi2 1844  tpi3 1845  snnz 1846  prnz 1847  tpnz 1848  el 1860  opnz 1897  opthwiener 1914  unieqi 1928  uni0 1938  unidif 1943  inteqi 1969  intmin2 1984  iuniin 2001  ssiin 2024  iinss 2025  iinun2 2031  iundif2 2032  iindif2 2033  iinuni 2036  iinpw 2038  breq1i 2068  breq2i 2069  biopabi 2103  opabsb 2114  ssopab2 2119  so 2152  supex 2157  supeui 2163  supcli 2164  supubi 2165  suplubi 2166  supnubi 2167  elon 2208  epweon 2239  onprc 2240  onuni 2251  inton 2281  onne0 2287  elsuc 2292  elsuc2 2293  sucon 2298  sucex 2303  sucid 2304  onord 2343  ontrc 2344  oneirr 2345  onss 2347  onelss 2348  onsuc 2353  onuniorsuc 2355  onuninsuc 2356  onun 2358  nnon 2380  elnn 2383  limom 2387  peano2b 2388  peano1 2390  find 2396  tfinds2 2405  opthprc 2457  brel 2459  relssi 2481  relsn 2485  relin 2491  reldif 2492  inopab 2495  inxp 2496  xpindi 2497  xpindir 2498  reli 2500  rele 2501  coeq1i 2504  coeq2i 2505  dmeqi 2532  dm0 2542  dmsn0 2543  dmsnsn0 2544  dmv 2546  dmsnsnsn 2548  rneqi 2556  resabs1 2592  residm 2594  dffr3 2620  relcnv 2624  intasym 2627  elxp4 2640  elxp5 2641  cnvin 2643  xp0 2652  relco 2658  cnvcnv 2661  co01 2664  coi2 2666  cnvexg 2669  cnvex 2670  coexg 2671  funi 2692  funres 2697  funcnvcnv 2701  funcnvuni 2706  funres11 2709  funcnvres 2710  funimaex 2716  resfunexg 2717  fnresdisj 2732  fnresi 2737  fnopabg 2745  fco 2760  fssres 2764  fint 2769  fconst 2774  f1cnv 2782  f1co 2783  f1oun 2815  f1oco 2816  ffoss 2820  f10 2822  f1oi 2825  f1ovi 2826  f1osn 2827  fveq1i 2833  fveq2i 2835  fvex 2838  elrnopab 2884  fopab2 2891  fnressn 2897  fressnfv 2898  fconst2 2902  fvclex 2908  fvresex 2909  isoid 2933  isomin 2937  isoini 2938  ncanth 2946  tfrlem6 2954  tfrlem10 2958  tfrlem13 2961  tz7.44lem1 2965  tz7.44-1 2966  tz7.44-2 2967  tz7.44-3 2968  rdgsucopabn 2985  frfnom 2989  frzer 2990  tz7.48-1 2994  tz7.48-2 2995  tz7.48-3 2996  tz7.49 2997  abianfp 3000  opreq1i 3009  opreq2i 3010  reloprab 3022  bioprabi 3027  reldmoprab 3034  funoprab 3037  fnoprab2 3039  dmoprab2 3040  elrnoprab 3054  ndmoprcl 3058  1stval 3089  2ndval 3090  fo1st 3094  fo2nd 3095  f1stres 3096  df1st2 3098  oev 3122  om0x 3126  oe0m 3127  oe0m0 3128  oa0r 3141  om0r 3142  o1p1e2 3143  oe1m 3147  oaordi 3148  oawordeulem 3156  oa00 3161  nnmsucr 3182  1onn 3193  2onn 3194  ecelqsi 3229  ecqs 3233  brecop2 3243  ecopoprdm 3245  th3qcor 3252  th3q 3253  mapprc 3260  elmap 3265  relen 3277  reldom 3278  relsdom 3279  breng 3280  brdomg 3281  bren 3282  brdom 3283  enref 3295  f1oen 3301  f1dom 3302  en2 3305  en3 3306  dom2 3308  dmen 3310  ssdomg 3311  ensym 3317  ensymi 3318  domtr 3320  f1imaen 3327  ensn1 3329  fundmen 3333  en2sn 3336  endisj 3341  undom 3342  xpdom2 3345  xpdom3 3347  pw2en 3348  sbthlem2 3350  sbthlem3 3351  sbthlem6 3354  sbthlem7 3355  sbthlem8 3356  sbthcl 3361  dom0 3367  sdom0 3369  canth2 3381  xpen 3383  mapdom1 3387  mapdom2lem 3388  xpmapenlem2 3392  xpmapenlem4 3394  mapunen 3397  pwen 3398  ssenen 3399  limenpsi 3400  limensuci 3401  phplem3 3405  php 3409  php2 3410  php3 3411  0sdom1dom 3420  ominf 3423  infsdomnn 3426  pssnn 3428  ssfi 3430  unblem4 3434  unbnn 3435  unbnn2 3436  unfilem1 3438  unfilem2 3439  unfilem3 3440  fiint 3445  eirrv 3449  eirr 3450  inf0 3457  inf1 3458  inf3lemb 3461  inf3lem6 3469  inf3 3471  inf5 3472  omex 3475  omenps 3482  omensuc 3483  trcl 3489  tz9.1 3490  zfregs 3491  r1fnon 3494  r1tr 3498  r1ord 3499  r1ord2 3500  tz9.12lem2 3504  tz9.12lem3 3505  unir1 3511  rankval 3512  rankval2 3514  rankid 3516  rankr1 3518  rankel 3524  rankval3 3525  rankpw 3528  rankss 3531  ranksn 3532  rankuni 3533  rankun 3535  r1rankid 3537  rankr1id 3539  ranklon 3540  scottex 3541  cplem2 3546  bnd 3548  karden 3551  aceq3lem 3555  aceq3 3556  aceq5lem3 3560  aceq5 3563  ac6lem 3575  kmlem2 3581  kmlem5 3584  kmlem10 3589  kmlem11 3590  kmlem16 3595  numthlem 3598  numth2 3600  numthcor 3601  weth 3602  zornlem2 3604  zornlem4 3606  zornlem6 3608  zornlem7 3609  fodom 3613  fodomb 3615  hta 3619  card0 3630  cardom 3632  cardid 3635  oncard 3636  cardsn 3640  carddomi 3641  unxpdomlem 3649  unxpdom2 3651  sucxpdom 3652  sdomsdomcard 3654  cardlim 3657  cardsdomel 3658  ondomon 3662  carduni 3664  cardprc 3667  alephfnon 3668  alephon 3671  alephsuc 3672  alephcard 3673  alephnbtwn 3674  alephnbtwn2 3675  aleph1 3676  alephordlem1 3677  alephordlem2 3678  alephordi 3679  alephord 3680  alephord2 3681  alephgeom 3687  alephislim 3688  isinfcard 3692  alephiso 3697  cffnon 3702  cfub 3703  cflim 3704  cardcf 3706  cflecard 3707  cfle 3708  cfsuc 3709  cfom 3710  uncdadom 3718  cdaen 3719  cda1en 3721  xp1en 3722  xp2cda 3723  cdacomen 3724  cdaassen 3725  xpcdaen 3726  cdadom1 3727  axpowndlem2 3744  axacndlem4 3756  zfcndpow 3762  zfcndinf 3764  dmaddpi 3812  dmmulpi 3813  1lt2pi 3826  indpi 3828  1q 3851  mulidpq 3863  recmulpq 3864  1lt2pq 3872  ltexpq 3874  halfpq 3876  ltbtwnpq 3878  1pr 3911  prlem934a 3931  prlem934b 3932  prlem934 3933  reclem3pr 3952  gt0srpr 3981  0r 3983  1r 3984  m1r 3985  m1m1sr 3996  recexsrlem 4006  ssgt0sr 4011  ltpsrpr 4013  suppsrlem 4015  suppsr 4016  supsrlem3 4021  supsrlem5 4023  addresr 4050  mulresr 4051  axresscn 4062  ax1id 4077  axi2m1 4082  axcnre 4087  addid1 4112  mulid1 4114  negex 4116  addcan 4120  negeu 4124  negeqi 4137  subcl 4139  negcl 4142  subadd 4143  renegcl 4171  mulm1 4205  mulcan 4207  receu 4215  divmul 4218  divcl 4221  divass 4242  redivcl 4274  ltlei 4303  ltnr 4338  leid 4339  gt0ne0i 4345  lt01 4377  ltplus1 4384  recgt0i 4385  prodgt0i 4387  divgt0i 4391  ltmul1i 4393  ltreci 4409  posex 4422  nnre 4429  nn1suc 4435  nngt0 4445  nnsub 4450  sup3i 4515  nnunb 4520  arch 4521  inelr 4527  nn0ssre 4538  0nn0 4546  nn0ge0i 4559  0z 4573  elnnz1 4581  1z 4584  2z 4585  halfnz 4586  elnn0nn 4593  uzind 4603  nn0ind 4612  om2uz0 4651  om2uzuz 4653  om2uzran 4655  om2uzf1o 4656  uzrdgval 4657  uzrdgini 4658  uzrdgsuc 4659  seqlem1 4662  seqval 4665  seq1lem 4668  seqsuclem 4669  0expt 4680  1expt 4681  sqval 4685  sqcl 4686  sqrecl 4699  discrlem1 4713  nnlesq 4718  nneo 4719  sqr0 4730  sqrlem2 4732  sqrlem6 4736  sqrlem7 4737  sqrlem8 4738  sqrlem13 4743  sqrlem16 4746  sqrlem18 4748  sqrlem20 4750  sqrmuli 4762  sqr1 4771  sqr2irrlem4 4780  sqr2re 4783  nthruz 4785  recl 4802  imcl 4803  cjcl 4804  replim 4805  crre 4806  crim 4807  cjcj 4808  cjre 4811  recj 4812  imcj 4813  cjadd 4818  cjmul 4819  cjneg 4827  addcj 4828  absval2 4836  absvalsq 4837  abscl 4840  absge0 4841  absneg 4843  abscj 4844  absmul 4846  absid 4850  leabs 4852  absor 4853  absre 4854  releabs 4858  abstri 4859  facnnt 4870  fac0 4871  fac1 4872  facp1t 4873  clim2 4881  clim0 4882  climunii 4883  ruclem5 4889  ruclem6 4890  ruclem7 4891  ruclem8 4892  ruclem10 4894  ruclem11 4895  ruclem13 4897  ruclem15 4899  ruclem17 4901  ruclem18 4902  ruclem19 4903  ruclem20 4904  ruclem21 4905  ruclem23 4907  ruclem24 4908  ruclem25 4909  ruclem26 4910  ruclem27 4911  ruclem28 4912  ruclem29 4913  ruclem30 4914  ruclem31 4915  ruclem32 4916  ruclem33 4917  ruclem35 4919  ruclem37 4921  ruclem39 4923  nnenom 4926  xpnnen 4927  znnen 4930  qnnen 4931  infxpidmlem1 4933  infxpidmlem8 4940  infxpidmlem11 4943  infxpidmlem12 4944  infunabs 4946  infcdaabs 4947  infdif 4948  infmap1 4950  infmap2lem2 4952  infmap2 4953  alephexp1 4954  alephsuc3 4955  alephexp2 4956  hvmul0t 5004  hvaddid2 5008  hvnegid 5009  hv2times 5033  hvnegdi 5034  hvsubeq0 5035  hvsubcan2 5036  hvsubadd 5038  hvsub0t 5041  hizer1t 5054  normlem5 5067  normlem6 5068  normlem7 5069  normlem8 5071  normlem7t 5072  bcseq 5073  norm0 5079  normcl 5081  normsq 5082  norm-i 5083  norm-ii 5086  norm-iii 5087  normsub 5089  norm3dif 5094  normpar2 5100  bcs 5101  hcauchy 5103  hlim2 5112  shssi 5119  chshi 5132  chlim 5139  hlim0 5140  hlimcaui 5141  hlimunii 5143  shsspwh 5153  hsn0elch 5155  ocvalt 5161  chocval 5178  chocuni 5179  occllem6 5185  occllem7 5186  occl 5188  projlem3 5195  projlem4 5196  projlem5 5197  projlem6 5198  projlem7 5199  projlem8 5200  projlem14 5206  projlem15 5207  projlem16 5208  projlem18 5210  projlem20 5212  projlem30 5222  projlem 5224  pjthlem1 5225  pjthlem2 5226  pjthlem3 5227  pjthlem7 5231  pjthlem12 5236  pjthlem13 5237  pjthlem14 5238  pjth 5239  omlsilem 5249  omlsi 5250  omls 5251  ococ 5252  pjcli 5257  pjhcli 5258  pjpj0 5259  pjoc1 5268  pjch 5269  pjoml 5271  pjococ 5272  shscl 5282  choc0 5291  choc1 5292  chocnul 5293  shintcl 5294  shintclt 5295  chintclt 5297  spanvalt 5300  hsupval2t 5301  chsupid 5312  sshjvalt 5321  sshjval3t 5327  shsvs 5337  shunss 5338  shslej 5339  shsidm 5358  shsumval2 5361  shsumval3 5362  shne0 5372  ch0le 5373  chle0 5374  chocin 5376  chlejb1 5397  shjshs 5412  chjidm 5437  span0 5448  spanun 5450  sshhococ 5451  chsup0 5453  h1deot 5454  h1det 5455  h1de2b 5459  h1de2ctlem 5460  h1de2ct 5461  spansn 5462  spansnch 5467  spansnpj 5481  spanunsn 5482  h1datom 5483  hosmvalt 5487  hodmvalt 5488  pjoml2 5495  pjoml4 5497  cmcmlem 5500  cmbr3 5509  cmbr4 5510  osumlem2 5531  osumlem4 5533  osumlem6 5535  osum 5538  spansnj 5539  spansncv 5542  5oa 5551  3oalem5 5556  3oalem6 5557  pjadj 5564  pjadd 5566  pjmul 5568  pjsslem 5570  pjss2 5571  pjssm 5572  pjdifnorm 5574  pj0 5581  pjocin 5583  pjfn 5586  pjoi0 5592  hoeq 5595  hoco 5598  hocofn 5601  hosfn 5604  ho0 5612  pjocco 5643  pjclem1 5649  pjclem4 5653  pjc 5654  pj3s 5659  pjnorm 5663  pjpyth 5664  pjnel 5665  stelt 5671  sto1 5677  stle 5681  strlem1 5691  strlem3a 5693  strlem4 5695  strlem5 5696  jplem2 5702  stcltrth 5711  hatomistic 5755  atcvat4 5775  sumdmdlem 5786

metamath.org