ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp2an Structured version   Unicode version

Theorem mp2an 402
Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
Hypotheses
Ref Expression
mp2an.1
mp2an.2
mp2an.3
Assertion
Ref Expression
mp2an

Proof of Theorem mp2an
StepHypRef Expression
1 mp2an.2 . 2
2 mp2an.1 . . 3
3 mp2an.3 . . 3
42, 3mpan 400 . 2
51, 4ax-mp 7 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  mp4an  403  jaoi  635  mp3an  1231  barbara  1995  eqeq12i  2050  vtocl2  2603  spc2ev  2642  sbc2ie  2823  csbieb  2882  sseq12i  2965  uneq12i  3089  ineq12i  3130  nelpri  3388  ralpr  3416  rexpr  3417  preq12i  3443  dfop  3539  opeq12i  3545  breq12i  3764  mpteq2ia  3834  opex  3957  opi2  3961  opth2  3968  otth2  3969  opeqsn  3980  opeqpr  3981  uniop  3983  opelopaba  3994  braba  3995  opelopab  3999  brab  4000  opelopabaf  4001  unex  4142  snnex  4147  op1stb  4175  onun2i  4183  onsucsssucexmid  4212  onsucelsucexmid  4215  opthreg  4234  tfis  4249  finds  4266  finds2  4267  nnregexmid  4285  xpeq12i  4310  opelvv  4333  eqrelriiv  4377  eqrelrdv  4379  relsnop  4387  xpss  4389  xpex  4396  relop  4429  brco  4449  opelcnv  4460  brcnv  4461  asymref  4653  codir  4656  ssrnres  4706  dmprop  4738  op2ndb  4747  dfco2  4763  cossxp  4786  coex  4806  funsn  4891  fnsn  4896  feq23i  4984  resasplitss  5012  fabex  5021  fvex  5138  xpsn  5282  fmptap  5296  fvsn  5301  opabex  5328  acexmidlemv  5453  oveq12i  5467  oprabid  5480  oprabss  5532  caovcom  5600  opabex3  5691  iunex  5692  oprabex  5697  ofmres  5705  op1st  5715  op2nd  5716  fo1st  5726  fo2nd  5727  mpt2ex  5778  1stconst  5784  2ndconst  5785  algrflem  5792  dftpos4  5819  tpostpos  5820  tpossym  5832  frecfnom  5925  sucinc  5964  fnoei  5971  oeiexg  5972  nnacli  6000  nnmcli  6001  elec  6081  ecovcom  6149  ecovass  6151  ecovdi  6153  entri  6202  endisj  6234  xpcomco  6236  ssfiexmid  6254  1lt2pi  6324  indpi  6326  1nq  6350  rec1nq  6379  1lt2nq  6389  ltaddnq  6390  halfnqq  6393  prarloclemarch2  6402  prarloclemlt  6476  prarloclemcalc  6485  genpelxp  6494  ltexprlempr  6582  recexprlempr  6604  cauappcvgprlemcl  6625  cauappcvgprlemladd  6630  caucvgprlemcl  6647  0r  6678  1sr  6679  m1r  6680  m1p1sr  6688  m1m1sr  6689  0lt1sr  6693  1ne0sr  6694  1idsr  6696  recexgt0sr  6701  pitonnlem1p1  6742  pitonnlem2  6743  axi2m1  6759  axprecex  6764  axcnre  6765  0cn  6817  addcli  6829  mulcli  6830  mulcomi  6831  readdcli  6838  remulcli  6839  rexpssxrxp  6867  ltrelxr  6877  gtneii  6910  lttri3i  6912  letri3i  6913  ltnsymi  6914  lenlti  6915  ltlei  6916  mulgt0i  6924  mulgt0ii  6925  0lt1  6938  addcomi  6954  pncan3oi  7024  resubcli  7070  subcli  7083  pncan3i  7084  negsubi  7085  subnegi  7086  subeq0i  7087  neg11i  7088  negcon1i  7089  negcon2i  7090  mulneg1i  7197  mulneg2i  7198  mul2negi  7199  addgt0ii  7278  ltnegi  7280  lenegi  7281  ltnegcon2i  7282  lesub0i  7283  ltaddposi  7284  posdifi  7285  ltnegcon1i  7286  lenegcon1i  7287  subge0i  7288  1ap0  7374  recrecapi  7502  dividapi  7503  div0api  7504  rec11apii  7519  divdiv32api  7525  recgt0ii  7654  ltrecii  7665  ltdiv23ii  7674  nnssre  7699  nnind  7711  nnmulcli  7717  nnsubi  7734  0le2  7786  1lt3  7866  2lt4  7868  1lt4  7869  3lt5  7871  2lt5  7872  1lt5  7873  4lt6  7875  3lt6  7876  2lt6  7877  1lt6  7878  5lt7  7880  4lt7  7881  3lt7  7882  2lt7  7883  1lt7  7884  6lt8  7886  5lt8  7887  4lt8  7888  3lt8  7889  2lt8  7890  1lt8  7891  7lt9  7893  6lt9  7894  5lt9  7895  4lt9  7896  3lt9  7897  2lt9  7898  1lt9  7899  8lt10  7901  7lt10  7902  6lt10  7903  5lt10  7904  4lt10  7905  3lt10  7906  2lt10  7907  1lt10  7908  2muline0  7927  nn0addcli  7995  nn0mulcli  7996  nn0addge1i  8006  nn0addge2i  8007  dfz2  8089  halfnz  8112  numnncl  8151  numltc  8163  nummac  8175  eluzaddi  8275  eluzsubi  8276  eluz2nn  8287  uzuzle23  8289  eluzge3nn  8290  divfnzn  8332  elq  8333  qreccl  8351  xrltnr  8471  mnfltpnf  8476  xrex  8526  elicc2i  8578  ioomax  8587  iccmax  8588  ioopos  8589  elxrge0  8617  iccshftri  8633  iccshftli  8635  iccdili  8637  icccntri  8639  unitssre  8643  fz10  8680  fzpreddisj  8703  frecfzennn  8884  m1expcl2  8931  m1expcl  8932  nn0expcli  8935  sqmuli  8989  cu2  9004  i3  9007  subsqi  9014  binom2subi  9018  rei  9127  imi  9128  readdi  9156  imaddi  9157  remuli  9158  immuli  9159  cjaddi  9160  cjmuli  9161  ipcni  9162  crrei  9164  crimi  9165  sqrt1  9216  sqrt4  9217  sqrt9  9218  abs1  9226  bj-unex  9372  bj-nn0suc0  9408  bj-nntrans  9409  bj-nnelirr  9411
  Copyright terms: Public domain W3C validator