ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp GIF version

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 𝜑 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.

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 𝜑
maj (𝜑𝜓)
Assertion
Ref Expression
ax-mp 𝜓

Detailed syntax breakdown of Axiom ax-mp
StepHypRef Expression
1 wps 1 wff 𝜓
Colors of variables: wff set class
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  2218  neeq2i  2219  necon3i  2250  rspec  2370  rgen2a  2372  mprg  2375  r19.21  2392  r19.23  2421  raleqi  2506  rexeqi  2507  elexi  2564  ceqsal  2580  vtocl3  2607  vtoclef  2623  vtocle  2624  spcv  2643  spcev  2644  clel3  2676  elabf  2683  elab2  2687  elab3  2691  euxfrdc  2724  reueq  2735  rmoimi2  2739  sbsbc  2765  sbc8g  2768  sbc6  2786  sbcie  2794  sbcrex  2834  csbvarg  2874  csbief  2888  csbie2  2892  sbnfc2  2903  sseli  2938  sselii  2939  sseq1i  2966  sseq2i  2967  psseq1i  3030  psseq2i  3031  difeq1i  3055  difeq2i  3056  uneq1i  3090  uneq2i  3091  ineq1i  3131  ineq2i  3132  ssinss1  3162  difdif2ss  3191  vn0  3228  vn0m  3229  abf  3257  npss0  3263  disj2  3272  difid  3289  0dif  3292  disjdif  3293  difin0  3294  undif1ss  3295  difdifdirss  3304  rgenm  3320  iftruei  3334  iffalsei  3337  ifbieq2i  3348  ifbieq12i  3350  pweqi  3360  pwid  3370  sneqi  3384  elsn  3388  elpr  3393  elsn2  3402  ralsn  3411  rexsn  3412  eltp  3415  r19.12sn  3433  rabrsndc  3435  preq1i  3447  preq2i  3448  prid1  3473  snnz  3484  snm  3485  prnz  3487  prm  3488  tpnz  3490  snsssn  3529  opeq1i  3549  opeq2i  3550  unieqi  3587  unissi  3600  inteqi  3616  intmin2  3638  intab  3641  intsn  3647  iinconstm  3663  iuniin  3664  iinss1  3666  iunxdif2  3702  ssiinf  3703  iinss  3705  iinss2  3706  iinab  3715  iundif2ss  3719  iindif2m  3721  iinin2m  3722  iunxsn  3730  iinpw  3739  sndisj  3757  disjxsn  3759  breqi  3767  breq1i  3768  breq2i  3769  brab1  3806  opabbii  3821  truni  3865  bm1.3ii  3875  a9evsep  3876  ax9vsep  3877  zfnuleu  3878  axnul  3879  ssexi  3892  rabex  3898  elpw2  3908  pwnss  3909  iin0r  3919  intv  3920  snex  3934  ord3ex  3938  dtruarb  3939  snelpw  3946  rext  3948  sspwb  3949  intid  3957  euabex  3958  mss  3959  exss  3960  opi1  3966  opnzi  3969  copsexg  3978  opeqsn  3986  opeqpr  3987  uniop  3989  opelopabf  4008  epelc  4025  elon  4098  inton  4117  onn0  4124  onm  4125  elsuc  4130  elsuc2  4131  sucid  4141  iunsuc  4144  onordi  4150  ontrci  4151  onelssi  4153  snnex  4168  eusvnf  4172  op1stb  4196  ssonunii  4202  sucex  4212  onssi  4228  onsuci  4229  ordtriexmidlem  4232  ordtriexmidlem2  4233  ordtriexmid  4234  ordtri2orexmid  4235  2ordpr  4236  ontr2exmid  4237  onsucsssucexmid  4239  onsucelsucexmid  4242  regexmidlemm  4244  ruALT  4260  onprc  4261  sucon  4262  dtruex  4268  dtru  4269  0elsucexmid  4274  ordpwsucexmid  4279  ordtri2or2exmid  4281  omex  4294  find  4300  omelon  4309  nnoni  4311  limom  4314  nnregexmid  4320  xpeq1i  4343  xpeq2i  4344  0nelxp  4350  opthprc  4369  mosubop  4384  releqi  4401  relssi  4409  relin1  4433  relin2  4434  reldif  4435  inopab  4446  difopab  4447  xpiindim  4451  opabbi2dv  4463  relop  4464  ideq  4466  coeq1i  4473  coeq2i  4474  cnveqi  4488  eldm  4510  eldm2  4511  dmeqi  4514  dmv  4529  rneqi  4540  elrnmpti  4565  dmex  4576  rnex  4577  reseq1i  4586  reseq2i  4587  residm  4620  resex  4629  resmpt3  4635  imaeq1i  4643  imaeq2i  4644  elima  4651  elimasn  4670  args  4672  epini  4674  dfse2  4676  relbrcnv  4683  cotr  4684  issref  4685  cnvsym  4686  asymref  4688  intirr  4689  codir  4691  qfto  4692  ssrnres  4741  cnveq0  4755  cnvsn0  4767  dmsnop  4772  rnsnop  4779  resdm2  4789  dfco2a  4799  cocnvcnv1  4809  coi2  4815  coires1  4816  cnvssrndm  4820  cossxp  4821  relrelss  4822  relcoi2  4826  unidmrn  4828  dfdm2  4830  unixpm  4831  cnvexg  4833  cnvex  4834  cnviinm  4837  iotaval  4856  funeqi  4900  funi  4910  funopg  4912  funres  4919  funcnvsn  4923  funcnvcnv  4936  funin  4948  funcnvres  4950  isarep2  4964  fneq1i  4971  fneq2i  4972  fnresdisj  4987  fnresi  4994  mpt0  5004  dmmpti  5006  feq1i  5017  feq2i  5018  fdmi  5029  fun2  5042  fssres  5044  resasplitss  5047  fintm  5053  fconst6  5064  f1ores  5119  foimacnv  5122  resdif  5126  funcocnv2  5129  f1ovi  5143  fveq1i  5157  fveq2i  5159  0fv  5186  fvun1  5217  fvopab3ig  5224  fvmptss2  5225  fndmdif  5250  fneqeql2  5254  f1oresrab  5307  fmptco  5308  fnressn  5327  fressnfv  5328  fmptap  5331  fvsnun1  5338  fvsnun2  5339  fsnunfv  5341  fconst2  5356  mptex  5365  riotabiia  5463  acexmidlema  5481  acexmidlemb  5482  acexmidlemcase  5485  acexmidlem2  5487  acexmidlemv  5488  oveq1i  5500  oveq2i  5501  oveqi  5503  oprabidlem  5514  0neqopab  5528  oprabbii  5538  oprabss  5568  mpt2mpt  5574  funoprab  5579  fnoprab  5582  fovcl  5584  ovigg  5599  elmpt2cl  5676  resfunexgALT  5715  cofunexg  5716  opabex3d  5726  opabex3  5727  1st0  5749  2nd0  5750  op1st  5751  op2nd  5752  fo1st  5762  fo2nd  5763  f1stres  5764  f2ndres  5765  fo1stresm  5766  fo2ndresm  5767  1stcof  5768  2ndcof  5769  1stexg  5772  2ndexg  5773  releldm2  5789  reldm  5790  dfoprab3  5795  mpt2mptsx  5801  mpt2mpts  5802  fnmpt2i  5808  dmmpt2  5809  mpt2exxg  5811  1stconst  5820  2ndconst  5821  dfmpt2  5822  algrflem  5828  algrflemg  5829  mpt2xopn0yelv  5832  mpt2xopoveq  5833  tposssxp  5842  brtpos2  5844  reldmtpos  5846  dftpos2  5854  dftpos4  5856  tpostpos  5857  tpostpos2  5858  tposfo  5864  tposf  5865  tposeqi  5870  tposex  5871  tposoprab  5873  issmo  5881  smores  5885  smores2  5887  iordsmo  5890  smo0  5891  tfrlem8  5912  tfrexlem  5926  tfri2  5930  rdgisuc1  5949  rdg0  5952  frec0g  5961  frecsuclem1  5965  frecsuclem2  5967  frecrdg  5970  2on0  5988  xp01disj  5995  2oconcl  6000  fnoa  6005  oaexg  6006  fnom  6008  omexg  6009  fnoei  6010  oeiexg  6011  oei0  6017  oacl  6018  oasuc  6022  o1p1e2  6026  omsuc  6029  nna0r  6035  nnm0r  6036  1onn  6071  2onn  6072  3onn  6073  4onn  6074  eqerlem  6115  elqs  6135  qsex  6141  ecqs  6146  iinerm  6156  th3qlem1  6186  th3q  6189  brdom  6209  f1dom  6218  enref  6223  dom2  6233  idssen  6235  ssdomg  6236  ensymi  6240  ensn1  6254  fiprc  6270  xpcomf1o  6277  xpcomco  6278  phplem2  6294  php5  6299  snnen2og  6300  php5dom  6303  ssfiexmid  6314  0fin  6319  diffitest  6321  findcard  6322  findcard2  6323  findcard2s  6324  ac6sfi  6329  card0  6340  0npi  6383  dmaddpi  6395  dmmulpi  6396  1lt2pi  6410  0nnq  6434  1nq  6436  dmaddpq  6449  dmmulpq  6450  rec1nq  6465  1lt2nq  6476  halfnqq  6480  prarloclemarch2  6489  enq0enq  6501  nqnq0pi  6508  nnnq0lem1  6516  addnnnq0  6519  mulnnnq0  6520  nq0m0r  6526  addpinq1  6534  prarloclem5  6570  prarloclemcalc  6572  1pr  6624  1idprl  6660  1idpru  6661  ltexprlemm  6670  recexprlem1ssl  6703  recexprlem1ssu  6704  prsrlem1  6799  addsrpr  6802  mulsrpr  6803  gt0srpr  6805  0nsr  6806  0r  6807  1sr  6808  m1r  6809  m1m1sr  6818  caucvgsr  6858  addresr  6885  mulresr  6886  pitonnlem1  6893  peano1nnnn  6900  axi2m1  6921  axcnre  6927  peano5nnnn  6938  axcaucvg  6946  mulid1i  7001  mulid2i  7002  pnfnre  7038  mnfnre  7039  rexri  7049  ltnri  7081  ltleii  7091  00id  7125  addid1i  7126  addid2i  7127  0cnALT  7172  negeqi  7176  negicn  7183  neg0  7227  renegcli  7243  negcli  7249  negidi  7250  negnegi  7251  subidi  7252  subid1i  7253  negne0bi  7254  negrebi  7255  mul02i  7357  mul01i  7358  mulm1i  7370  leidi  7446  gt0ne0ii  7448  inelr  7542  msqge0i  7575  gt0ap0ii  7585  1div1e1  7648  div1i  7683  eqnegi  7684  recclapi  7685  recidapi  7686  divmulapi  7709  rerecclapi  7720  redivclapi  7722  recgt0  7783  ltp1i  7838  divgt0ii  7852  ltmul1ii  7861  ltdiv1ii  7862  peano5nni  7884  nnrei  7890  1nn  7892  nngt0i  7911  neg1ap0  7991  2timesi  8005  times2i  8006  2nn  8042  3nn  8043  4nn  8044  5nn  8045  6nn  8046  7nn  8047  8nn  8048  9nn  8049  10nn  8050  2muline0  8114  rehalfcli  8137  nn0ssre  8148  nnnn0i  8152  dfn2  8157  0nn0  8159  nn0ge0i  8172  zrei  8214  neg1z  8240  nn0negzi  8243  dfz2  8276  nneoi  8305  peano5uzi  8310  dfuzi  8311  nn0ind-raph  8318  deceq1i  8335  deceq2i  8336  numltc  8350  eluzel2  8441  eluz1i  8443  nn0uz  8470  nnuz  8471  lbzbi  8514  divfnzn  8519  qdivcl  8539  irrmul  8543  cnref1o  8544  mnfxr  8652  pnfnemnf  8655  0ltpnf  8661  mnflt0  8663  0lepnf  8669  xrltnsym  8672  xrlttri3  8676  nltpnft  8688  ngtmnft  8689  xrrebnd  8690  xnegmnf  8700  xneg0  8702  xltnegi  8706  ixxex  8726  iooval2  8742  unirnioo  8800  ioorebasg  8802  elrege0  8803  fzval2  8835  fzen  8865  fzprval  8902  fztpval  8903  uzdisj  8913  ige2m1fz  8930  fz0tp  8939  nn0disj  8953  1fv  8954  4fvwrd4  8955  fzo0ss1  8988  fzo01  9030  fzo12sn  9031  fzo0to2pr  9032  fzo0to3tp  9033  fzo0to42pr  9034  frechashgf1o  9074  iser0f  9120  0exp0e1  9129  qexpcl  9140  qexpclz  9145  m1expcl2  9146  1exp  9153  sqvali  9202  sqcli  9203  sqeq0i  9204  resqcli  9207  sq1  9216  neg1sqe1  9217  shftidt2  9302  cjexp  9362  re0  9364  im0  9365  re1  9366  im1  9367  cj0  9370  cji  9371  recli  9380  imcli  9381  cjcli  9382  replimi  9383  cjcji  9384  reim0bi  9385  rerebi  9386  cjrebi  9387  recji  9388  imcji  9389  cjmulrcli  9390  cjmulvali  9391  cjmulge0i  9392  renegi  9393  imnegi  9394  cjnegi  9395  addcji  9396  uzin2  9455  rexanuz  9456  sqrtrval  9467  sqrt0  9471  resqrexlemcalc3  9483  resqrexlemcvg  9486  resqrex  9493  abs0  9525  absi  9526  absimle  9549  recan  9574  caubnd2  9582  leabsi  9593  absrei  9594  sqrtpclii  9595  sqrtgt0ii  9596  absvalsqi  9605  absvalsq2i  9606  abscli  9607  absge0i  9608  absval2i  9609  abs00i  9610  absgt0api  9611  absnegi  9612  abscji  9613  releabsi  9614  elabf2  9785  bd0  9808  bdeli  9830  bdcriota  9867  bdbm1.3ii  9875  bdinex1  9883  bdssexi  9887  bj-inex  9891  bj-snex  9897  bj-sucex  9907  bj-notbii  9910  bj-d0clsepcl  9913  bj-omind  9922  bj-om  9925  bj-2inf  9926  bj-peano2  9927  bdpeano5  9932  bj-omssonALT  9952  bj-inf2vnlem1  9959  bj-omex2  9966  bj-nn0sucALT  9967
  Copyright terms: Public domain W3C validator