ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-mp Unicode 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  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
StepHypRef Expression
1 wps 1  wff  ps
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  109  simpri  111  biimpi  118  bicomi  130  mpbi  143  mpbir  144  imbi1i  236  a1bi  241  tbt  245  biantru  296  biantrur  297  mp2an  417  pm2.65i  601  notnoti  607  pm2.21i  608  pm2.24ii  609  notbii  627  nbn  648  ori  675  orci  683  olci  684  biorfi  698  imorri  701  simp1i  948  simp2i  949  simp3i  950  3mix1i  1111  3mix2i  1112  3mix3i  1113  3jaoi  1235  trud  1294  dfnot  1303  mptnan  1355  mtpor  1357  mtpxor  1358  mpg  1381  19.23h  1428  hbequid  1447  axi12  1448  nfri  1453  spi  1470  19.21  1516  eximii  1534  19.35i  1557  nfn  1589  19.37aiv  1606  19.23  1609  exan  1624  equid  1630  hbae  1648  equvini  1683  equveli  1684  sbid  1699  sbieh  1715  exdistrfor  1723  dveeq2or  1739  ax11v  1750  ax11ev  1751  equs5or  1753  sb4or  1756  sb4bor  1758  nfsb2or  1760  sbequilem  1761  sbequi  1762  speiv  1785  nfsbxy  1861  nfsbxyt  1862  sbco  1885  sbcocom  1887  sbcomxyyz  1889  elsb3  1895  elsb4  1896  sbal1yz  1920  dvelimALT  1929  dvelimfv  1930  dvelimor  1937  eumoi  1976  moani  2013  eqeq1i  2090  eqeq2i  2093  eleq1i  2148  eleq2i  2149  nfcrii  2216  neeq1i  2264  neeq2i  2265  necon3i  2297  rspec  2420  rgen2a  2422  mprg  2425  r19.21  2442  r19.23  2473  raleqi  2558  rexeqi  2559  rabeqif  2601  elexi  2620  ceqsal  2637  vtocl3  2664  vtoclef  2680  vtocle  2681  spcv  2700  spcev  2701  clel3  2738  elabf  2745  elab2  2749  elab3  2753  euxfrdc  2787  reueq  2798  rmoimi2  2802  sbsbc  2828  sbc8g  2831  sbc6  2849  sbcie  2857  sbcrex  2902  csbvarg  2942  csbief  2956  csbie2  2960  sbnfc2  2971  sseli  3004  sselii  3005  sseq1i  3032  sseq2i  3033  difeq1i  3096  difeq2i  3097  uneq1i  3132  uneq2i  3133  ineq1i  3179  ineq2i  3180  ssinss1  3210  difdif2ss  3237  vn0  3274  vn0m  3275  abf  3303  disj2  3315  difid  3328  0dif  3331  disjdif  3332  difin0  3333  undif1ss  3334  difdifdirss  3343  rgenm  3360  iftruei  3374  iffalsei  3377  ifbieq2i  3389  ifbieq12i  3391  pweqi  3404  pwid  3414  sneqi  3428  elsn  3432  elpr  3437  elsn2  3446  ralsn  3454  rexsn  3455  eltp  3458  rabrsndc  3478  preq1i  3490  preq2i  3491  prid1  3516  snnz  3527  snm  3528  prnz  3530  prm  3531  tpnz  3533  snsssn  3573  opeq1i  3593  opeq2i  3594  unieqi  3631  unissi  3644  inteqi  3660  intmin2  3682  intab  3685  intsn  3691  iinconstm  3707  iuniin  3708  iinss1  3710  iunxdif2  3746  ssiinf  3747  iinss  3749  iinss2  3750  iinab  3759  iundif2ss  3763  iindif2m  3765  iinin2m  3766  iunxsn  3774  iinpw  3783  sndisj  3801  disjxsn  3803  breqi  3811  breq1i  3812  breq2i  3813  brab1  3850  opabbii  3865  truni  3909  bm1.3ii  3919  a9evsep  3920  ax9vsep  3921  zfnuleu  3922  axnul  3923  ssexi  3936  rabex  3942  elpw2  3952  pwnss  3953  iin0r  3963  intv  3964  snex  3977  ord3ex  3981  dtruarb  3982  undifexmid  3984  intid  4007  opnzi  4018  copsexg  4027  opelopabf  4057  epelc  4074  elon  4157  inton  4176  onn0  4183  onm  4184  elsuc  4189  elsuc2  4190  sucid  4200  iunsuc  4203  onordi  4209  ontrci  4210  onelssi  4212  eusvnf  4231  ssonunii  4261  sucex  4271  onssi  4287  onsuci  4288  ordtriexmidlem  4291  ordtriexmidlem2  4292  ordtriexmid  4293  ordtri2orexmid  4294  2ordpr  4295  ontr2exmid  4296  onsucsssucexmid  4298  onsucelsucexmid  4301  regexmidlemm  4303  reg2exmid  4307  onirri  4314  ruALT  4322  onprc  4323  sucon  4324  dtru  4331  0elsucexmid  4336  ordpwsucexmid  4341  ordtri2or2exmid  4342  omex  4362  find  4368  omelon  4377  nnoni  4379  limom  4382  nnregexmid  4388  xpeq1i  4411  xpeq2i  4412  0nelxp  4418  opthprc  4437  mosubop  4452  releqi  4469  relssi  4477  relin1  4503  relin2  4504  reldif  4505  inopab  4516  difopab  4517  xpiindim  4521  opabbi2dv  4533  ideq  4536  coeq1i  4543  coeq2i  4544  cnveqi  4558  eldm  4580  eldm2  4581  dmeqi  4584  dmv  4599  rneqi  4610  elrnmpti  4635  dmex  4646  rnex  4647  reseq1i  4656  reseq2i  4657  residm  4690  resex  4699  resmpt3  4707  imaeq1i  4715  imaeq2i  4716  elima  4723  elimasn  4742  args  4744  epini  4746  dfse2  4748  relbrcnv  4755  cotr  4756  issref  4757  cnvsym  4758  asymref  4760  intirr  4761  codir  4763  qfto  4764  ssrnres  4813  cnveq0  4827  cnvsn0  4839  dmsnop  4844  rnsnop  4851  resdm2  4861  dfco2a  4871  cocnvcnv1  4881  coi2  4887  coires1  4888  cnvssrndm  4892  cossxp  4893  relrelss  4894  relcoi2  4898  unidmrn  4900  dfdm2  4902  unixpm  4903  cnvexg  4905  cnvex  4906  cnviinm  4909  iotaval  4928  funeqi  4972  funi  4982  funres  4991  funcnvsn  4995  funcnvcnv  5009  funin  5021  funcnvres  5023  isarep2  5037  fneq1i  5044  fneq2i  5045  fnresdisj  5060  fnresi  5067  mpt0  5077  dmmpti  5079  feq1i  5090  feq2i  5091  fdmi  5102  fun2  5115  fssres  5117  resasplitss  5120  fintm  5126  fconst6  5137  f1ores  5192  foimacnv  5195  resdif  5199  funcocnv2  5202  f1ovi  5216  fveq1i  5230  fveq2i  5232  0fv  5260  fvun1  5291  fvopab3ig  5298  fvmptss2  5299  fndmdif  5324  fneqeql2  5328  f1oresrab  5381  fmptco  5382  fnressn  5401  fressnfv  5402  fmptap  5405  fvsnun1  5412  fvsnun2  5413  fsnunfv  5415  fconst2  5430  mptex  5439  riotabiia  5536  acexmidlema  5554  acexmidlemb  5555  acexmidlemcase  5558  acexmidlem2  5560  acexmidlemv  5561  oveq1i  5573  oveq2i  5574  oveqi  5576  oprabidlem  5587  0neqopab  5601  oprabbii  5611  oprabss  5641  mpt2mpt  5647  funoprab  5652  fnoprab  5655  fovcl  5657  ovigg  5672  elmpt2cl  5749  resfunexgALT  5788  cofunexg  5789  opabex3d  5799  opabex3  5800  1st0  5822  2nd0  5823  op1st  5824  op2nd  5825  f1stres  5837  f2ndres  5838  fo1stresm  5839  fo2ndresm  5840  1stcof  5841  2ndcof  5842  1stexg  5845  2ndexg  5846  releldm2  5862  reldm  5863  dfoprab3  5868  mpt2mptsx  5874  mpt2mpts  5875  fnmpt2i  5881  dmmpt2  5882  mpt2exxg  5884  1stconst  5893  2ndconst  5894  dfmpt2  5895  algrflem  5901  algrflemg  5902  cnvoprab  5906  f1od2  5907  mpt2xopn0yelv  5908  mpt2xopoveq  5909  tposssxp  5918  brtpos2  5920  reldmtpos  5922  dftpos2  5930  dftpos4  5932  tpostpos  5933  tpostpos2  5934  tposfo  5940  tposf  5941  tposeqi  5946  tposex  5947  tposoprab  5949  issmo  5957  smores  5961  smores2  5963  iordsmo  5966  smo0  5967  tfrlem8  5987  tfrexlem  6003  tfr1onlem3  6007  tfr1onlemsucaccv  6010  tfr1onlembxssdm  6012  tfr1onlemres  6018  tfri1dALT  6020  tfri2  6035  rdgisuc1  6053  rdg0  6056  frecfun  6064  frec0g  6066  freccllem  6071  frecfcllem  6073  frecsuclem  6075  frecrdg  6077  2on0  6094  xp01disj  6101  2oconcl  6106  fnoa  6111  oaexg  6112  fnom  6114  omexg  6115  fnoei  6116  oeiexg  6117  oei0  6123  oacl  6124  oasuc  6128  o1p1e2  6132  omsuc  6136  nna0r  6142  nnm0r  6143  1onn  6180  2onn  6181  3onn  6182  4onn  6183  eqerlem  6224  elqs  6244  qsex  6250  ecqs  6255  iinerm  6265  th3qlem1  6295  th3q  6298  brdom  6318  f1dom  6328  enref  6333  dom2  6343  idssen  6345  ssdomg  6346  ensymi  6350  ensn1  6364  fiprc  6381  1domsn  6384  xpcomf1o  6390  xpcomco  6391  phplem2  6409  php5  6414  snnen2og  6415  1nen2  6417  php5dom  6419  ssfilem  6431  ssfiexmid  6432  domfiexmid  6434  0fin  6440  diffitest  6443  findcard  6444  findcard2  6445  findcard2s  6446  isinfinf  6453  ac6sfi  6454  inffiexmid  6457  unfiexmid  6462  xpfi  6472  fisseneq  6474  ssfirab  6475  en1eqsn  6487  supeq1i  6495  infeq1i  6520  djurf1o  6555  djuun  6558  card0  6568  0npi  6617  dmaddpi  6629  dmmulpi  6630  1lt2pi  6644  0nnq  6668  1nq  6670  dmaddpq  6683  dmmulpq  6684  rec1nq  6699  1lt2nq  6710  halfnqq  6714  prarloclemarch2  6723  enq0enq  6735  nqnq0pi  6742  nnnq0lem1  6750  addnnnq0  6753  mulnnnq0  6754  nq0m0r  6760  addpinq1  6768  prarloclem5  6804  prarloclemcalc  6806  1pr  6858  1idprl  6894  1idpru  6895  ltexprlemm  6904  recexprlem1ssl  6937  recexprlem1ssu  6938  prsrlem1  7033  addsrpr  7036  mulsrpr  7037  gt0srpr  7039  0nsr  7040  0r  7041  1sr  7042  m1r  7043  m1m1sr  7052  caucvgsr  7092  addresr  7119  mulresr  7120  pitonnlem1  7127  peano1nnnn  7134  axi2m1  7155  axcnre  7161  peano5nnnn  7172  axcaucvg  7180  mulid1i  7235  mulid2i  7236  pnfnre  7274  mnfnre  7275  pnfnemnf  7287  mnfxr  7289  rexri  7290  ltnri  7322  ltleii  7332  00id  7368  addid1i  7369  addid2i  7370  0cnALT  7417  negeqi  7421  negicn  7428  neg0  7473  renegcli  7489  negcli  7495  negidi  7496  negnegi  7497  subidi  7498  subid1i  7499  negne0bi  7500  negrebi  7501  mul02i  7613  mul01i  7614  mulm1i  7626  leidi  7705  gt0ne0ii  7707  inelr  7803  msqge0i  7836  gt0ap0ii  7846  1div1e1  7911  div1i  7947  eqnegi  7948  recclapi  7949  recidapi  7950  divmulapi  7973  rerecclapi  7984  redivclapi  7986  recgt0  8047  ltp1i  8102  divgt0ii  8116  ltmul1ii  8125  ltdiv1ii  8126  peano5nni  8161  nnrei  8167  1nn  8169  nngt0i  8188  neg1ap0  8267  2timesi  8281  times2i  8282  2nn  8312  3nn  8313  4nn  8314  5nn  8315  6nn  8316  7nn  8317  8nn  8318  9nn  8319  2muline0  8375  rehalfcli  8398  nn0ssre  8411  nnnn0i  8415  dfn2  8420  0nn0  8422  nn0ge0i  8434  zrei  8490  neg1z  8516  nn0negzi  8519  dfz2  8553  nneoi  8584  peano5uzi  8589  dfuzi  8590  nn0ind-raph  8597  deceq1i  8616  deceq2i  8617  10nn  8625  numltc  8635  eluzel2  8757  eluz1i  8759  nn0uz  8786  nnuz  8787  infrenegsupex  8815  lbzbi  8834  divfnzn  8839  qdivcl  8861  irrmul  8865  cnref1o  8866  0ltpnf  8985  mnflt0  8987  0lepnf  8993  xrltnsym  8996  xrlttri3  9000  nltpnft  9012  ngtmnft  9013  xrrebnd  9014  xnegmnf  9024  xneg0  9026  xltnegi  9030  ixxex  9050  iooval2  9066  unirnioo  9124  ioorebasg  9126  elrege0  9127  fzval2  9160  fzen  9190  fzprval  9227  fztpval  9228  uzdisj  9238  ige2m1fz  9255  fz01or  9256  fz0tp  9264  nn0disj  9277  1fv  9278  4fvwrd4  9279  fzo0ss1  9312  fzo01  9354  fzo12sn  9355  fzo0to2pr  9356  fzo0to3tp  9357  fzo0to42pr  9358  qbtwnxr  9396  flval  9406  modqfrac  9471  modqmulnn  9476  q2txmodxeq0  9518  frecuzrdgdom  9552  frecuzrdgfun  9554  frecuzrdgsuct  9558  frechashgf1o  9562  nnct  9569  iseqvalcbv  9583  iser0f  9621  0exp0e1  9630  qexpcl  9641  qexpclz  9646  m1expcl2  9647  1exp  9654  sqvali  9704  sqcli  9705  sqeq0i  9706  resqcli  9709  sq1  9718  neg1sqe1  9719  iexpcyc  9728  facnn  9803  fac0  9804  fac1  9805  fac2  9807  fac3  9808  fac4  9809  bcval  9825  bcm1k  9836  ibcval5  9839  bcpasc  9842  bccl  9843  4bc3eq4  9849  4bc2eq6  9850  hashinfom  9854  hashennn  9856  hashfz1  9859  fihasheq0  9870  hash0  9873  hashsng  9874  fihashen1  9875  omgadd  9878  hashp1i  9886  hashxp  9902  shftidt2  9921  cjexp  9981  re0  9983  im0  9984  re1  9985  im1  9986  cj0  9989  cji  9990  recli  9999  imcli  10000  cjcli  10001  replimi  10002  cjcji  10003  reim0bi  10004  rerebi  10005  cjrebi  10006  recji  10007  imcji  10008  cjmulrcli  10009  cjmulvali  10010  cjmulge0i  10011  renegi  10012  imnegi  10013  cjnegi  10014  addcji  10015  uzin2  10074  rexanuz  10075  rexfiuz  10076  sqrtrval  10087  sqrt0  10091  resqrexlemcalc3  10103  resqrexlemcvg  10106  resqrex  10113  abs0  10145  absi  10146  qabsor  10162  absimle  10171  recan  10196  caubnd2  10204  leabsi  10215  absrei  10216  sqrtpclii  10217  sqrtgt0ii  10218  absvalsqi  10227  absvalsq2i  10228  abscli  10229  absge0i  10230  absval2i  10231  abs00i  10232  absgt0api  10233  absnegi  10234  abscji  10235  releabsi  10236  0dvds  10423  dvds1  10461  z0even  10518  n2dvdsm1  10520  z2even  10521  n2dvds3  10522  ndvdssub  10537  ndvdsi  10540  flodddiv4  10541  gcddvds  10562  gcd1  10585  6gcd4e2  10591  bezoutlembi  10601  dfgcd3  10606  dfgcd2  10610  eucialg  10648  lcmval  10652  lcmcllem  10656  lcmledvds  10659  3lcm2e6woprm  10675  qredeu  10686  isprm2lem  10705  isprm3  10707  prm2orodd  10715  pw2dvds  10751  phicl2  10797  phi1  10802  dfphi2  10803  phiprmpw  10805  ex-fl  10823  ex-ceil  10824  ex-fac  10825  ex-gcd  10828  elabf2  10852  bd0  10882  bdeli  10904  bdcriota  10941  bdbm1.3ii  10949  bdinex1  10957  bdssexi  10961  bj-inex  10965  bj-snex  10971  bj-sucex  10981  bj-notbii  10984  bj-d0clsepcl  10987  bj-omind  10996  bj-om  10999  bj-2inf  11000  bj-peano2  11001  bdpeano5  11005  bj-omssonALT  11025  bj-inf2vnlem1  11032  bj-omex2  11039  bj-nn0sucALT  11040
  Copyright terms: Public domain W3C validator