ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mp2an Structured version   GIF 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  6475  prarloclemcalc  6484  genpelxp  6493  ltexprlempr  6581  recexprlempr  6603  cauappcvgprlemcl  6624  cauappcvgprlemladd  6629  0r  6658  1sr  6659  m1r  6660  m1p1sr  6668  m1m1sr  6669  0lt1sr  6673  1ne0sr  6674  1idsr  6676  recexgt0sr  6681  pitonnlem1p1  6722  pitonnlem2  6723  axi2m1  6739  axprecex  6744  axcnre  6745  0cn  6797  addcli  6809  mulcli  6810  mulcomi  6811  readdcli  6818  remulcli  6819  rexpssxrxp  6847  ltrelxr  6857  gtneii  6890  lttri3i  6892  letri3i  6893  ltnsymi  6894  lenlti  6895  ltlei  6896  mulgt0i  6904  mulgt0ii  6905  0lt1  6918  addcomi  6934  pncan3oi  7004  resubcli  7050  subcli  7063  pncan3i  7064  negsubi  7065  subnegi  7066  subeq0i  7067  neg11i  7068  negcon1i  7069  negcon2i  7070  mulneg1i  7177  mulneg2i  7178  mul2negi  7179  addgt0ii  7258  ltnegi  7260  lenegi  7261  ltnegcon2i  7262  lesub0i  7263  ltaddposi  7264  posdifi  7265  ltnegcon1i  7266  lenegcon1i  7267  subge0i  7268  1ap0  7354  recrecapi  7482  dividapi  7483  div0api  7484  rec11apii  7499  divdiv32api  7505  recgt0ii  7634  ltrecii  7645  ltdiv23ii  7654  nnssre  7679  nnind  7691  nnmulcli  7697  nnsubi  7714  0le2  7766  1lt3  7846  2lt4  7848  1lt4  7849  3lt5  7851  2lt5  7852  1lt5  7853  4lt6  7855  3lt6  7856  2lt6  7857  1lt6  7858  5lt7  7860  4lt7  7861  3lt7  7862  2lt7  7863  1lt7  7864  6lt8  7866  5lt8  7867  4lt8  7868  3lt8  7869  2lt8  7870  1lt8  7871  7lt9  7873  6lt9  7874  5lt9  7875  4lt9  7876  3lt9  7877  2lt9  7878  1lt9  7879  8lt10  7881  7lt10  7882  6lt10  7883  5lt10  7884  4lt10  7885  3lt10  7886  2lt10  7887  1lt10  7888  2muline0  7907  nn0addcli  7975  nn0mulcli  7976  nn0addge1i  7986  nn0addge2i  7987  dfz2  8069  halfnz  8092  numnncl  8131  numltc  8143  nummac  8155  eluzaddi  8255  eluzsubi  8256  eluz2nn  8267  uzuzle23  8269  eluzge3nn  8270  divfnzn  8312  elq  8313  qreccl  8331  xrltnr  8451  mnfltpnf  8456  xrex  8506  elicc2i  8558  ioomax  8567  iccmax  8568  ioopos  8569  elxrge0  8597  iccshftri  8613  iccshftli  8615  iccdili  8617  icccntri  8619  unitssre  8623  fz10  8660  fzpreddisj  8683  frecfzennn  8864  m1expcl2  8911  m1expcl  8912  nn0expcli  8915  sqmuli  8969  cu2  8984  i3  8987  subsqi  8994  binom2subi  8998  rei  9107  imi  9108  readdi  9136  imaddi  9137  remuli  9138  immuli  9139  cjaddi  9140  cjmuli  9141  ipcni  9142  crrei  9144  crimi  9145  sqrt1  9196  sqrt4  9197  sqrt9  9198  abs1  9206  bj-unex  9350  bj-nn0suc0  9384  bj-nntrans  9385  bj-nnelirr  9387
  Copyright terms: Public domain W3C validator