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  104  simpri  106  biimpi  113  bicomi  123  mpbi  133  mpbir  134  imbi1i  227  a1bi  232  tbt  236  biantru  286  biantrur  287  mp2an  402  pm2.65i  568  notnoti  574  pm2.21i  575  pm2.24ii  576  notbii  594  nbn  615  ori  642  orci  650  olci  651  biorfi  665  imorri  668  simp1i  913  simp2i  914  simp3i  915  3mix1i  1076  3mix2i  1077  3mix3i  1078  3jaoi  1198  trud  1252  dfnot  1262  mptnan  1314  mtpor  1316  mtpxor  1317  mpg  1340  19.23h  1387  hbequid  1406  axi12  1407  nfri  1412  spi  1429  19.21  1475  eximii  1493  19.35i  1516  nfn  1548  19.37aiv  1565  19.23  1568  exan  1583  equid  1589  hbae  1606  equvini  1641  equveli  1642  sbid  1657  sbieh  1673  exdistrfor  1681  dveeq2or  1697  ax11v  1708  ax11ev  1709  equs5or  1711  sb4or  1714  sb4bor  1716  nfsb2or  1718  sbequilem  1719  sbequi  1720  speiv  1742  nfsbxy  1818  nfsbxyt  1819  sbco  1842  sbcocom  1844  sbcomxyyz  1846  elsb3  1852  elsb4  1853  sbal1yz  1877  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  eumoi  1933  moani  1970  eqeq1i  2047  eqeq2i  2050  eleq1i  2103  eleq2i  2104  nfcrii  2171  neeq1i  2220  neeq2i  2221  necon3i  2253  rspec  2373  rgen2a  2375  mprg  2378  r19.21  2395  r19.23  2424  raleqi  2509  rexeqi  2510  elexi  2567  ceqsal  2583  vtocl3  2610  vtoclef  2626  vtocle  2627  spcv  2646  spcev  2647  clel3  2679  elabf  2686  elab2  2690  elab3  2694  euxfrdc  2727  reueq  2738  rmoimi2  2742  sbsbc  2768  sbc8g  2771  sbc6  2789  sbcie  2797  sbcrex  2837  csbvarg  2877  csbief  2891  csbie2  2895  sbnfc2  2906  sseli  2941  sselii  2942  sseq1i  2969  sseq2i  2970  psseq1i  3033  psseq2i  3034  difeq1i  3058  difeq2i  3059  uneq1i  3093  uneq2i  3094  ineq1i  3134  ineq2i  3135  ssinss1  3165  difdif2ss  3194  vn0  3231  vn0m  3232  abf  3260  npss0  3266  disj2  3275  difid  3292  0dif  3295  disjdif  3296  difin0  3297  undif1ss  3298  difdifdirss  3307  rgenm  3323  iftruei  3337  iffalsei  3340  ifbieq2i  3351  ifbieq12i  3353  pweqi  3363  pwid  3373  sneqi  3387  elsn  3391  elpr  3396  elsn2  3405  ralsn  3414  rexsn  3415  eltp  3418  r19.12sn  3436  rabrsndc  3438  preq1i  3450  preq2i  3451  prid1  3476  snnz  3487  snm  3488  prnz  3490  prm  3491  tpnz  3493  snsssn  3532  opeq1i  3552  opeq2i  3553  unieqi  3590  unissi  3603  inteqi  3619  intmin2  3641  intab  3644  intsn  3650  iinconstm  3666  iuniin  3667  iinss1  3669  iunxdif2  3705  ssiinf  3706  iinss  3708  iinss2  3709  iinab  3718  iundif2ss  3722  iindif2m  3724  iinin2m  3725  iunxsn  3733  iinpw  3742  sndisj  3760  disjxsn  3762  breqi  3770  breq1i  3771  breq2i  3772  brab1  3809  opabbii  3824  truni  3868  bm1.3ii  3878  a9evsep  3879  ax9vsep  3880  zfnuleu  3881  axnul  3882  ssexi  3895  rabex  3901  elpw2  3911  pwnss  3912  iin0r  3922  intv  3923  snex  3937  ord3ex  3941  dtruarb  3942  snelpw  3949  rext  3951  sspwb  3952  intid  3960  euabex  3961  mss  3962  exss  3963  opi1  3969  opnzi  3972  copsexg  3981  opeqsn  3989  opeqpr  3990  uniop  3992  opelopabf  4011  epelc  4028  elon  4111  inton  4130  onn0  4137  onm  4138  elsuc  4143  elsuc2  4144  sucid  4154  iunsuc  4157  onordi  4163  ontrci  4164  onelssi  4166  snnex  4181  eusvnf  4185  op1stb  4209  ssonunii  4215  sucex  4225  onssi  4241  onsuci  4242  ordtriexmidlem  4245  ordtriexmidlem2  4246  ordtriexmid  4247  ordtri2orexmid  4248  2ordpr  4249  ontr2exmid  4250  onsucsssucexmid  4252  onsucelsucexmid  4255  regexmidlemm  4257  reg2exmid  4261  ruALT  4275  onprc  4276  sucon  4277  dtruex  4283  dtru  4284  0elsucexmid  4289  ordpwsucexmid  4294  ordtri2or2exmid  4296  omex  4316  find  4322  omelon  4331  nnoni  4333  limom  4336  nnregexmid  4342  xpeq1i  4365  xpeq2i  4366  0nelxp  4372  opthprc  4391  mosubop  4406  releqi  4423  relssi  4431  relin1  4455  relin2  4456  reldif  4457  inopab  4468  difopab  4469  xpiindim  4473  opabbi2dv  4485  relop  4486  ideq  4488  coeq1i  4495  coeq2i  4496  cnveqi  4510  eldm  4532  eldm2  4533  dmeqi  4536  dmv  4551  rneqi  4562  elrnmpti  4587  dmex  4598  rnex  4599  reseq1i  4608  reseq2i  4609  residm  4642  resex  4651  resmpt3  4657  imaeq1i  4665  imaeq2i  4666  elima  4673  elimasn  4692  args  4694  epini  4696  dfse2  4698  relbrcnv  4705  cotr  4706  issref  4707  cnvsym  4708  asymref  4710  intirr  4711  codir  4713  qfto  4714  ssrnres  4763  cnveq0  4777  cnvsn0  4789  dmsnop  4794  rnsnop  4801  resdm2  4811  dfco2a  4821  cocnvcnv1  4831  coi2  4837  coires1  4838  cnvssrndm  4842  cossxp  4843  relrelss  4844  relcoi2  4848  unidmrn  4850  dfdm2  4852  unixpm  4853  cnvexg  4855  cnvex  4856  cnviinm  4859  iotaval  4878  funeqi  4922  funi  4932  funopg  4934  funres  4941  funcnvsn  4945  funcnvcnv  4958  funin  4970  funcnvres  4972  isarep2  4986  fneq1i  4993  fneq2i  4994  fnresdisj  5009  fnresi  5016  mpt0  5026  dmmpti  5028  feq1i  5039  feq2i  5040  fdmi  5051  fun2  5064  fssres  5066  resasplitss  5069  fintm  5075  fconst6  5086  f1ores  5141  foimacnv  5144  resdif  5148  funcocnv2  5151  f1ovi  5165  fveq1i  5179  fveq2i  5181  0fv  5208  fvun1  5239  fvopab3ig  5246  fvmptss2  5247  fndmdif  5272  fneqeql2  5276  f1oresrab  5329  fmptco  5330  fnressn  5349  fressnfv  5350  fmptap  5353  fvsnun1  5360  fvsnun2  5361  fsnunfv  5363  fconst2  5378  mptex  5387  riotabiia  5485  acexmidlema  5503  acexmidlemb  5504  acexmidlemcase  5507  acexmidlem2  5509  acexmidlemv  5510  oveq1i  5522  oveq2i  5523  oveqi  5525  oprabidlem  5536  0neqopab  5550  oprabbii  5560  oprabss  5590  mpt2mpt  5596  funoprab  5601  fnoprab  5604  fovcl  5606  ovigg  5621  elmpt2cl  5698  resfunexgALT  5737  cofunexg  5738  opabex3d  5748  opabex3  5749  1st0  5771  2nd0  5772  op1st  5773  op2nd  5774  fo1st  5784  fo2nd  5785  f1stres  5786  f2ndres  5787  fo1stresm  5788  fo2ndresm  5789  1stcof  5790  2ndcof  5791  1stexg  5794  2ndexg  5795  releldm2  5811  reldm  5812  dfoprab3  5817  mpt2mptsx  5823  mpt2mpts  5824  fnmpt2i  5830  dmmpt2  5831  mpt2exxg  5833  1stconst  5842  2ndconst  5843  dfmpt2  5844  algrflem  5850  algrflemg  5851  mpt2xopn0yelv  5854  mpt2xopoveq  5855  tposssxp  5864  brtpos2  5866  reldmtpos  5868  dftpos2  5876  dftpos4  5878  tpostpos  5879  tpostpos2  5880  tposfo  5886  tposf  5887  tposeqi  5892  tposex  5893  tposoprab  5895  issmo  5903  smores  5907  smores2  5909  iordsmo  5912  smo0  5913  tfrlem8  5934  tfrexlem  5948  tfri2  5952  rdgisuc1  5971  rdg0  5974  frec0g  5983  frecsuclem1  5987  frecsuclem2  5989  frecrdg  5992  2on0  6010  xp01disj  6017  2oconcl  6022  fnoa  6027  oaexg  6028  fnom  6030  omexg  6031  fnoei  6032  oeiexg  6033  oei0  6039  oacl  6040  oasuc  6044  o1p1e2  6048  omsuc  6051  nna0r  6057  nnm0r  6058  1onn  6093  2onn  6094  3onn  6095  4onn  6096  eqerlem  6137  elqs  6157  qsex  6163  ecqs  6168  iinerm  6178  th3qlem1  6208  th3q  6211  brdom  6231  f1dom  6240  enref  6245  dom2  6255  idssen  6257  ssdomg  6258  ensymi  6262  ensn1  6276  fiprc  6292  xpcomf1o  6299  xpcomco  6300  phplem2  6316  php5  6321  snnen2og  6322  php5dom  6325  ssfiexmid  6336  0fin  6341  diffitest  6344  findcard  6345  findcard2  6346  findcard2s  6347  ac6sfi  6352  card0  6368  0npi  6411  dmaddpi  6423  dmmulpi  6424  1lt2pi  6438  0nnq  6462  1nq  6464  dmaddpq  6477  dmmulpq  6478  rec1nq  6493  1lt2nq  6504  halfnqq  6508  prarloclemarch2  6517  enq0enq  6529  nqnq0pi  6536  nnnq0lem1  6544  addnnnq0  6547  mulnnnq0  6548  nq0m0r  6554  addpinq1  6562  prarloclem5  6598  prarloclemcalc  6600  1pr  6652  1idprl  6688  1idpru  6689  ltexprlemm  6698  recexprlem1ssl  6731  recexprlem1ssu  6732  prsrlem1  6827  addsrpr  6830  mulsrpr  6831  gt0srpr  6833  0nsr  6834  0r  6835  1sr  6836  m1r  6837  m1m1sr  6846  caucvgsr  6886  addresr  6913  mulresr  6914  pitonnlem1  6921  peano1nnnn  6928  axi2m1  6949  axcnre  6955  peano5nnnn  6966  axcaucvg  6974  mulid1i  7029  mulid2i  7030  pnfnre  7067  mnfnre  7068  rexri  7078  ltnri  7110  ltleii  7120  00id  7154  addid1i  7155  addid2i  7156  0cnALT  7201  negeqi  7205  negicn  7212  neg0  7257  renegcli  7273  negcli  7279  negidi  7280  negnegi  7281  subidi  7282  subid1i  7283  negne0bi  7284  negrebi  7285  mul02i  7387  mul01i  7388  mulm1i  7400  leidi  7477  gt0ne0ii  7479  inelr  7575  msqge0i  7608  gt0ap0ii  7618  1div1e1  7681  div1i  7716  eqnegi  7717  recclapi  7718  recidapi  7719  divmulapi  7742  rerecclapi  7753  redivclapi  7755  recgt0  7816  ltp1i  7871  divgt0ii  7885  ltmul1ii  7894  ltdiv1ii  7895  peano5nni  7917  nnrei  7923  1nn  7925  nngt0i  7944  neg1ap0  8026  2timesi  8040  times2i  8041  2nn  8077  3nn  8078  4nn  8079  5nn  8080  6nn  8081  7nn  8082  8nn  8083  9nn  8084  10nn  8085  2muline0  8150  rehalfcli  8173  nn0ssre  8185  nnnn0i  8189  dfn2  8194  0nn0  8196  nn0ge0i  8209  zrei  8251  neg1z  8277  nn0negzi  8280  dfz2  8313  nneoi  8342  peano5uzi  8347  dfuzi  8348  nn0ind-raph  8355  deceq1i  8372  deceq2i  8373  numltc  8387  eluzel2  8478  eluz1i  8480  nn0uz  8507  nnuz  8508  lbzbi  8551  divfnzn  8556  qdivcl  8577  irrmul  8581  cnref1o  8582  mnfxr  8694  pnfnemnf  8697  0ltpnf  8703  mnflt0  8705  0lepnf  8711  xrltnsym  8714  xrlttri3  8718  nltpnft  8730  ngtmnft  8731  xrrebnd  8732  xnegmnf  8742  xneg0  8744  xltnegi  8748  ixxex  8768  iooval2  8784  unirnioo  8842  ioorebasg  8844  elrege0  8845  fzval2  8877  fzen  8907  fzprval  8944  fztpval  8945  uzdisj  8955  ige2m1fz  8972  fz0tp  8981  nn0disj  8995  1fv  8996  4fvwrd4  8997  fzo0ss1  9030  fzo01  9072  fzo12sn  9073  fzo0to2pr  9074  fzo0to3tp  9075  fzo0to42pr  9076  flval  9116  modqfrac  9179  modqmulnn  9184  frechashgf1o  9205  iser0f  9251  0exp0e1  9260  qexpcl  9271  qexpclz  9276  m1expcl2  9277  1exp  9284  sqvali  9333  sqcli  9334  sqeq0i  9335  resqcli  9338  sq1  9347  neg1sqe1  9348  shftidt2  9433  cjexp  9493  re0  9495  im0  9496  re1  9497  im1  9498  cj0  9501  cji  9502  recli  9511  imcli  9512  cjcli  9513  replimi  9514  cjcji  9515  reim0bi  9516  rerebi  9517  cjrebi  9518  recji  9519  imcji  9520  cjmulrcli  9521  cjmulvali  9522  cjmulge0i  9523  renegi  9524  imnegi  9525  cjnegi  9526  addcji  9527  uzin2  9586  rexanuz  9587  sqrtrval  9598  sqrt0  9602  resqrexlemcalc3  9614  resqrexlemcvg  9617  resqrex  9624  abs0  9656  absi  9657  absimle  9680  recan  9705  caubnd2  9713  leabsi  9724  absrei  9725  sqrtpclii  9726  sqrtgt0ii  9727  absvalsqi  9736  absvalsq2i  9737  abscli  9738  absge0i  9739  absval2i  9740  abs00i  9741  absgt0api  9742  absnegi  9743  abscji  9744  releabsi  9745  ex-fl  9895  ex-ceil  9896  elabf2  9921  bd0  9944  bdeli  9966  bdcriota  10003  bdbm1.3ii  10011  bdinex1  10019  bdssexi  10023  bj-inex  10027  bj-snex  10033  bj-sucex  10043  bj-notbii  10046  bj-d0clsepcl  10049  bj-omind  10058  bj-om  10061  bj-2inf  10062  bj-peano2  10063  bdpeano5  10068  bj-omssonALT  10088  bj-inf2vnlem1  10095  bj-omex2  10102  bj-nn0sucALT  10103