Axiom ax-mp 7

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 ph is true, and ph implies ps, then ps must also be true." This rule is sometimes called "detachment," since it detaches the minor premise from the major premise.

Note: In some web page displays such as the Statement List, the symbols "&" and "=>" informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies." They are not part of the formal language. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
min	|- ph
maj	|- ( ph -> ps )

Assertion

Ref	Expression
ax-mp	|- ps

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff ps

This axiom is referenced by:  mp2b  8  a1i  9  mp1i  10  a2i  11  mpd  13  mp2  16  idALT  20  simpli  110  simpri  112  biimpi  119  bicomi  131  mpbi  144  mpbir  145  imbi1i  237  a1bi  242  tbt  246  biantru  298  biantrur  299  mp2an  420  pm2.65i  611  notnoti  617  pm2.21i  618  pm2.24ii  619  notbii  640  nbn  671  ori  695  orci  703  olci  704  biorfi  718  imorri  721  dcbii  808  simp1i  971  simp2i  972  simp3i  973  3mix1i  1134  3mix2i  1135  3mix3i  1136  3jaoi  1262  mptru  1321  dfnot  1330  mptnan  1382  mtpor  1384  mtpxor  1385  mpg  1408  19.23h  1455  hbequid  1474  axi12  1475  nfri  1480  spi  1497  19.21  1543  eximii  1562  19.35i  1585  nfn  1617  19.37aiv  1634  19.23  1637  exan  1652  equid  1658  hbae  1677  equvini  1712  equveli  1713  sbid  1728  sbieh  1744  exdistrfor  1752  dveeq2or  1768  ax11v  1779  ax11ev  1780  equs5or  1782  sb4or  1785  sb4bor  1787  nfsb2or  1789  sbequilem  1790  sbequi  1791  speiv  1814  nfsbxy  1891  nfsbxyt  1892  sbco  1915  sbcocom  1917  sbcomxyyz  1919  elsb3  1925  elsb4  1926  sbal1yz  1950  dvelimALT  1959  dvelimfv  1960  dvelimor  1967  eumoi  2006  moani  2043  eqeq1i  2120  eqeq2i  2123  eleq1i  2178  eleq2i  2179  nfcrii  2246  neeq1i  2295  neeq2i  2296  necon3i  2328  rspec  2456  rgen2a  2458  mprg  2461  r19.21  2480  r19.23  2512  raleqi  2602  rexeqi  2603  rabeqif  2646  elv  2659  elexi  2667  ceqsal  2684  vtocl3  2711  vtoclef  2728  vtocle  2729  spcv  2748  spcev  2749  clel3  2788  elabf  2795  elab2  2799  elab3  2803  euxfrdc  2837  reueq  2850  rmoimi2  2854  sbsbc  2880  sbc8g  2883  sbc6  2901  sbcie  2909  sbcrex  2954  csbvarg  2994  csbief  3008  csbie2  3013  sbnfc2  3024  sseli  3057  sselii  3058  sseq1i  3087  sseq2i  3088  difeq1i  3154  difeq2i  3155  uneq1i  3190  uneq2i  3191  ineq1i  3237  ineq2i  3238  ssinss1  3269  difdif2ss  3297  n0ii  3335  ne0ii  3336  vn0  3337  vn0m  3338  abf  3370  disj2  3382  difid  3395  0dif  3398  disjdif  3399  difin0  3400  undif1ss  3401  difdifdirss  3411  rgenm  3429  iftruei  3444  iffalsei  3447  ifbieq2i  3459  ifbieq12i  3461  pweqi  3478  pwid  3489  sneqi  3503  elsn  3507  elpr  3512  elsn2  3523  ralsn  3531  rexsn  3532  eltp  3535  rabrsndc  3555  preq1i  3567  preq2i  3568  prid1  3593  snnz  3606  snm  3607  prnz  3609  prm  3610  tpnz  3612  snsssn  3652  opeq1i  3672  opeq2i  3673  unieqi  3710  unissi  3723  inteqi  3739  intmin2  3761  intab  3764  intsn  3770  iinconstm  3786  iuniin  3787  iinss1  3789  iunxdif2  3825  ssiinf  3826  iinss  3828  iinss2  3829  iinab  3838  iundif2ss  3842  iindif2m  3844  iinin2m  3845  iunxsn  3853  iunxprg  3857  iinpw  3867  sndisj  3889  disjxsn  3891  breqi  3899  breq1i  3900  breq2i  3901  brab1  3938  opabbii  3953  truni  3998  bm1.3ii  4007  a9evsep  4008  ax9vsep  4009  zfnuleu  4010  axnul  4011  ssexi  4024  rabex  4030  elpw2  4040  pwnss  4041  iin0r  4051  intv  4052  pwex  4065  snex  4067  notnotsnex  4069  ord3ex  4072  dtruarb  4073  undifexmid  4075  intid  4104  opnzi  4115  copsexg  4124  opelopabf  4154  epelc  4171  elon  4254  inton  4273  onn0  4280  onm  4281  elsuc  4286  elsuc2  4287  sucid  4297  iunsuc  4300  onordi  4306  ontrci  4307  onelssi  4309  eusvnf  4332  ssonunii  4363  sucex  4373  onssi  4389  onsuci  4390  ordtriexmidlem  4393  ordtriexmidlem2  4394  ordtriexmid  4395  ordtri2orexmid  4396  2ordpr  4397  ontr2exmid  4398  onsucsssucexmid  4400  onsucelsucexmid  4403  regexmidlemm  4405  reg2exmid  4409  onirri  4416  ruALT  4424  onprc  4425  sucon  4426  dtru  4433  0elsucexmid  4438  ordpwsucexmid  4443  ordtri2or2exmid  4444  dcextest  4453  omex  4465  find  4471  omelon  4480  nnoni  4482  limom  4485  nnregexmid  4492  omsinds  4493  xpeq1i  4517  xpeq2i  4518  0nelxp  4525  opthprc  4548  mosubop  4563  releqi  4580  relssi  4588  relin1  4615  relin2  4616  reldif  4617  inopab  4629  difopab  4630  xpiindim  4634  opabbi2dv  4646  ideq  4649  coeq1i  4656  coeq2i  4657  cnveqi  4672  eldm  4694  eldm2  4695  dmeqi  4698  dmv  4713  rneqi  4725  elrnmpti  4750  dmex  4761  rnex  4762  reseq1i  4771  reseq2i  4772  residm  4807  resex  4816  resmpt3  4824  imaeq1i  4834  imaeq2i  4835  elima  4842  imaex  4850  elimasn  4862  args  4864  epini  4866  dfse2  4868  relbrcnv  4875  cotr  4876  issref  4877  cnvsym  4878  asymref  4880  intirr  4881  codir  4883  qfto  4884  ssrnres  4937  cnveq0  4951  cnvsn0  4963  dmsnop  4968  rnsnop  4975  resdm2  4985  dfco2a  4995  cocnvcnv1  5005  coi2  5011  coires1  5012  cnvssrndm  5016  cossxp  5017  cocnvres  5019  relrelss  5021  relcoi2  5025  unidmrn  5027  dfdm2  5029  unixpm  5030  cnvexg  5032  cnvex  5033  cnviinm  5036  iotaval  5055  funeqi  5100  funi  5111  funres  5120  funcnvsn  5124  funcnvcnv  5138  funin  5150  funcnvres  5152  isarep2  5166  fneq1i  5173  fneq2i  5174  fnresdisj  5189  fnresi  5196  mpt0  5206  dmmpti  5208  feq1i  5221  feq2i  5222  fdmi  5236  fun2  5252  fssres  5254  resasplitss  5258  fintm  5264  fconst6  5278  f1ores  5336  foimacnv  5339  resdif  5343  funcocnv2  5346  f1ovi  5360  fveq1i  5374  fveq2i  5376  0fv  5408  fvun1  5439  fvopab3ig  5447  fvmptss2  5448  mptrcl  5455  elfvmptrab1  5467  fndmdif  5477  fneqeql2  5481  f1oresrab  5537  fmptco  5538  fnressn  5558  fressnfv  5559  fmptap  5562  fvsnun1  5569  fvsnun2  5570  fsnunfv  5573  fconst2  5589  mptex  5598  riotabiia  5699  acexmidlema  5717  acexmidlemb  5718  acexmidlemcase  5721  acexmidlem2  5723  acexmidlemv  5724  oveq1i  5736  oveq2i  5737  oveqi  5739  oprabidlem  5754  0neqopab  5768  oprabbii  5778  oprabss  5809  mpompt  5815  funoprab  5823  fnoprab  5826  fovcl  5828  ovigg  5843  elmpocl  5920  resfunexgALT  5960  cofunexg  5961  opabex3d  5971  opabex3  5972  1st0  5994  2nd0  5995  op1st  5996  op2nd  5997  f1stres  6009  f2ndres  6010  fo1stresm  6011  fo2ndresm  6012  1stcof  6013  2ndcof  6014  1stexg  6017  2ndexg  6018  releldm2  6035  reldm  6036  dfoprab3  6041  mpomptsx  6047  mpompts  6048  fnmpoi  6054  dmmpo  6055  mpoexxg  6060  1stconst  6070  2ndconst  6071  dfmpo  6072  algrflem  6078  algrflemg  6079  cnvoprab  6083  f1od2  6084  mpoxopn0yelv  6088  mpoxopoveq  6089  tposssxp  6098  brtpos2  6100  reldmtpos  6102  dftpos2  6110  dftpos4  6112  tpostpos  6113  tpostpos2  6114  tposfo  6120  tposf  6121  tposeqi  6126  tposex  6127  tposoprab  6129  issmo  6137  smores  6141  smores2  6143  iordsmo  6146  smo0  6147  tfrlem8  6167  tfrexlem  6183  tfr1onlem3  6187  tfr1onlemsucaccv  6190  tfr1onlembxssdm  6192  tfr1onlemres  6198  tfri1dALT  6200  tfri2  6215  rdgisuc1  6233  rdg0  6236  frecfun  6244  frec0g  6246  freccllem  6251  frecfcllem  6253  frecsuclem  6255  frecrdg  6257  2on0  6275  xp01disj  6282  2oconcl  6288  fnoa  6295  oaexg  6296  fnom  6298  omexg  6299  fnoei  6300  oeiexg  6301  oei0  6307  oacl  6308  oasuc  6312  o1p1e2  6316  omsuc  6320  nna0r  6326  nnm0r  6327  1onn  6368  2onn  6369  3onn  6370  4onn  6371  eqerlem  6412  elqs  6432  qsex  6438  ecqs  6443  iinerm  6453  th3qlem1  6483  th3q  6486  mapsn  6536  mapsnf1o3  6543  ixpiinm  6570  ixpssmap  6578  brdom  6596  f1dom  6606  enref  6611  dom2  6621  idssen  6623  ssdomg  6624  ensymi  6628  ensn1  6642  fiprc  6661  1domsn  6664  xpcomf1o  6670  xpcomco  6671  dom0  6683  0dom  6684  xpmapenlem  6694  phplem2  6698  php5  6703  snnen2og  6704  1nen2  6706  php5dom  6708  ssfilem  6720  ssfiexmid  6721  domfiexmid  6723  0fin  6729  diffitest  6732  findcard  6733  findcard2  6734  findcard2s  6735  isinfinf  6742  ac6sfi  6743  inffiexmid  6751  unfiexmid  6757  xpfi  6769  fisseneq  6771  ssfirab  6772  en1eqsn  6786  snexxph  6788  sbthlem2  6796  sbthlemi3  6797  sbthlemi6  6800  sbthlem7  6801  fi0  6813  supeq1i  6825  infeq1i  6850  djuexb  6879  djuf1olemr  6889  inresflem  6895  djuinr  6898  updjudhcoinlf  6915  updjudhcoinrg  6916  casefun  6920  caserel  6922  caseinj  6924  caseinl  6926  caseinr  6927  omp1eomlem  6929  endjusym  6931  difinfsn  6935  difinfinf  6936  djuinj  6941  0ct  6942  ctmlemr  6943  ctssdclemn0  6945  ctssdccl  6946  finomni  6960  exmidomni  6962  fodjuomni  6969  nnnninf  6971  ctssexmid  6972  fodjumkv  6981  card0  6991  dju1p1e2  6998  exmidfodomrlemim  7002  exmidfodomrlemr  7003  exmidfodomrlemrALT  7004  0npi  7063  dmaddpi  7075  dmmulpi  7076  1lt2pi  7090  0nnq  7114  1nq  7116  dmaddpq  7129  dmmulpq  7130  rec1nq  7145  1lt2nq  7156  halfnqq  7160  prarloclemarch2  7169  enq0enq  7181  nqnq0pi  7188  nnnq0lem1  7196  addnnnq0  7199  mulnnnq0  7200  nq0m0r  7206  addpinq1  7214  prarloclem5  7250  prarloclemcalc  7252  1pr  7304  1idprl  7340  1idpru  7341  ltexprlemm  7350  recexprlem1ssl  7383  recexprlem1ssu  7384  prsrlem1  7479  addsrpr  7482  mulsrpr  7483  gt0srpr  7485  0nsr  7486  0r  7487  1sr  7488  m1r  7489  m1m1sr  7498  caucvgsr  7538  addresr  7566  mulresr  7567  pitonnlem1  7574  peano1nnnn  7581  axi2m1  7604  axcnre  7610  peano5nnnn  7621  axcaucvg  7629  mulid1i  7686  mulid2i  7687  pnfnre  7725  mnfnre  7726  pnfnemnf  7738  mnfxr  7740  rexri  7741  ltnri  7773  ltleii  7783  00id  7820  addid1i  7821  addid2i  7822  0cnALT  7869  negeqi  7873  negicn  7880  neg0  7925  renegcli  7941  negcli  7947  negidi  7948  negnegi  7949  subidi  7950  subid1i  7951  negne0bi  7952  negrebi  7953  mul02i  8065  mul01i  8066  mulm1i  8078  leidi  8160  gt0ne0ii  8162  inelr  8258  msqge0i  8291  gt0ap0ii  8302  1div1e1  8371  div1i  8407  eqnegi  8408  recclapi  8409  recidapi  8410  divmulapi  8433  rerecclapi  8444  redivclapi  8446  recgt0  8512  ltp1i  8567  divgt0ii  8581  ltmul1ii  8590  ltdiv1ii  8591  sup3exmid  8619  peano5nni  8627  nnrei  8633  1nn  8635  nngt0i  8654  neg1ap0  8733  2timesi  8748  times2i  8749  2nn  8779  3nn  8780  4nn  8781  5nn  8782  6nn  8783  7nn  8784  8nn  8785  9nn  8786  2muline0  8843  rehalfcli  8866  nn0ssre  8879  nnnn0i  8883  dfn2  8888  0nn0  8890  nn0ge0i  8902  zrei  8958  neg1z  8984  nn0negzi  8987  dfz2  9021  nneoi  9053  peano5uzi  9058  dfuzi  9059  nn0ind-raph  9066  deceq1i  9086  deceq2i  9087  10nn  9095  numltc  9105  eluzel2  9227  eluz1i  9229  nn0uz  9256  nnuz  9257  infrenegsupex  9285  lbzbi  9304  divfnzn  9309  qdivcl  9331  irrmul  9335  cnref1o  9336  0ltpnf  9455  mnflt0  9457  0lepnf  9463  xrltnsym  9466  xrlttri3  9470  nltpnft  9484  ngtmnft  9487  xrrebnd  9489  xnegmnf  9499  xneg0  9501  xltnegi  9505  xaddmnf1  9518  xaddmnf2  9519  mnfaddpnf  9521  xaddid1  9532  xnn0lenn0nn0  9535  xnn0xadd0  9537  xposdif  9552  ixxex  9569  iooval2  9585  unirnioo  9643  ioorebasg  9645  elrege0  9646  fzval2  9680  fzen  9710  fzprval  9749  fztpval  9750  uzdisj  9760  ige2m1fz  9777  fz01or  9778  fz1ssfz0  9784  fz0tp  9788  nn0disj  9802  1fv  9803  4fvwrd4  9804  fzo0ss1  9838  fzo01  9880  fzo12sn  9881  fzo0to2pr  9882  fzo0to3tp  9883  fzo0to42pr  9884  qbtwnxr  9922  flval  9932  modqfrac  9997  modqmulnn  10002  q2txmodxeq0  10044  frecuzrdgdom  10078  frecuzrdgfun  10080  frecuzrdgsuct  10084  frechashgf1o  10088  nnct  10095  fxnn0nninf  10098  0tonninf  10099  1tonninf  10100  iseqvalcbv  10117  ser0f  10175  0exp0e1  10185  qexpcl  10196  qexpclz  10201  m1expcl2  10202  1exp  10209  sqvali  10259  sqcli  10260  sqeq0i  10261  resqcli  10264  sq1  10273  neg1sqe1  10274  iexpcyc  10284  facnn  10360  fac0  10361  fac1  10362  fac2  10364  fac3  10365  fac4  10366  bcval  10382  bcm1k  10393  bcpasc  10399  bccl  10400  4bc3eq4  10406  4bc2eq6  10407  hashinfom  10411  hashennn  10413  hashfz1  10416  fihasheq0  10427  hash0  10430  hashsng  10431  fihashen1  10432  omgadd  10435  hashp1i  10443  hashxp  10459  fimaxq  10460  zfz1iso  10471  shftidt2  10491  cjexp  10552  re0  10554  im0  10555  re1  10556  im1  10557  cj0  10560  cji  10561  recli  10570  imcli  10571  cjcli  10572  replimi  10573  cjcji  10574  reim0bi  10575  rerebi  10576  cjrebi  10577  recji  10578  imcji  10579  cjmulrcli  10580  cjmulvali  10581  cjmulge0i  10582  renegi  10583  imnegi  10584  cjnegi  10585  addcji  10586  uzin2  10645  rexanuz  10646  rexfiuz  10647  sqrtrval  10658  sqrt0  10662  resqrexlemcalc3  10674  resqrexlemcvg  10677  resqrex  10684  abs0  10716  absi  10717  qabsor  10733  absimle  10742  recan  10767  caubnd2  10775  leabsi  10786  absrei  10787  sqrtpclii  10788  sqrtgt0ii  10789  absvalsqi  10798  absvalsq2i  10799  abscli  10800  absge0i  10801  absval2i  10802  abs00i  10803  absgt0api  10804  absnegi  10805  abscji  10806  releabsi  10807  infxrnegsupex  10918  xrbdtri  10931  cbvsum  11015  sumeq1i  11018  sum0  11043  isumz  11044  fisumss  11047  fsumsersdc  11050  fsumadd  11061  isumclim  11076  isumclim3  11078  fsumcnv  11092  modfsummodlem1  11111  fsumrelem  11126  binomlem  11138  binom  11139  arisum2  11154  expcnv  11159  0.999...  11176  ef0lem  11211  esum  11213  ere  11221  ege2le3  11222  ef0  11223  eff2  11231  efsep  11242  reeff1  11252  sin0  11281  cos0  11282  ef01bndlem  11308  cos2bnd  11312  sincos1sgn  11316  sincos2sgn  11317  sin4lt0  11318  eirr  11327  0dvds  11355  dvds1  11393  z0even  11450  n2dvdsm1  11452  z2even  11453  n2dvds3  11454  ndvdssub  11469  ndvdsi  11472  flodddiv4  11473  gcddvds  11494  gcd1  11517  6gcd4e2  11523  bezoutlembi  11533  dfgcd3  11538  dfgcd2  11542  lcmval  11584  lcmcllem  11588  lcmledvds  11591  3lcm2e6woprm  11607  qredeu  11618  isprm2lem  11637  isprm3  11639  prm2orodd  11647  pw2dvds  11683  phicl2  11729  phi1  11734  dfphi2  11735  phiprmpw  11737  ennnfonelemp1  11758  ennnfonelem1  11759  ennnfonelemkh  11764  ennnfonelemex  11766  ennnfonelemnn0  11774  ennnfonelemr  11775  exmidunben  11778  ctinfomlemom  11779  ctinfom  11780  ctinf  11782  qnnen  11783  structcnvcnv  11812  structfun  11814  structfn  11815  ndxarg  11819  ndxid  11820  setsresg  11834  setsslnid  11847  strleun  11885  strle1g  11886  istopon  12017  topontopi  12020  toponunii  12021  toponrestid  12025  istps  12036  topontopn  12041  eltpsi  12045  eltg4i  12061  eltg3  12063  tg1  12065  tg2  12066  tgclb  12071  topnex  12092  sn0topon  12094  distps  12097  cldrcl  12108  sn0cld  12143  restco  12180  lmrcl  12197  ssidcn  12215  cnconst2  12238  cnptopresti  12243  cnptoprest  12244  txuni2  12261  txbas  12263  eltx  12264  txcnp  12276  upxp  12277  txcnmpt  12278  uptx  12279  txcn  12280  txrest  12281  txlm  12284  cnmptid  12286  cnmpt1st  12293  cnmpt2nd  12294  psmetge0  12314  ismeti  12329  xmetunirn  12341  xmetge0  12348  unirnblps  12405  unirnbl  12406  mopnex  12488  qtopbasss  12504  retop  12507  uniretop  12508  iooretopg  12511  cnxmet  12514  cntoptopon  12515  cnbl0  12517  rexmet  12521  blssioo  12525  tgioo  12526  tgqioo  12527  limcresi  12585  dvfvalap  12599  dvidlemap  12609  dvcnp2cntop  12612  ex-fl  12621  ex-ceil  12622  ex-exp  12623  ex-fac  12624  ex-gcd  12627  bj-dcdc  12649  bj-stdc  12650  bj-dcst  12651  bj-stst  12652  elabf2  12672  bd0  12705  bdeli  12727  bdcriota  12764  bdbm1.3ii  12772  bdinex1  12780  bdssexi  12784  bj-inex  12788  bj-snex  12794  bj-sucex  12804  bj-d0clsepcl  12806  bj-omind  12815  bj-om  12818  bj-2inf  12819  bj-peano2  12820  bdpeano5  12824  bj-omssonALT  12844  bj-inf2vnlem1  12851  bj-omex2  12858  bj-nn0sucALT  12859  nninfall  12885  nninfsellemqall  12892  nninfsellemeqinf  12893  nninfomnilem  12895  nninfomni  12896  exmidsbthrlem  12898  sbthom  12902  isomninnlem  12906  isomninn  12907  cvgcmp2nlemabs  12908  trilpolemisumle  12912  trilpolemeq1  12914  trilpo  12917