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

Theorem mp2an 404
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 402 . 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  405  jaoi  623  mp3an  1215  barbara  1976  eqeq12i  2031  vtocl2  2582  spc2ev  2621  sbc2ie  2802  csbieb  2861  sseq12i  2944  uneq12i  3068  ineq12i  3109  nelpri  3367  ralpr  3395  rexpr  3396  preq12i  3422  dfop  3518  opeq12i  3524  breq12i  3743  mpteq2ia  3813  opex  3936  opi2  3940  opth2  3947  otth2  3948  opeqsn  3959  opeqpr  3960  uniop  3962  opelopaba  3973  braba  3974  opelopab  3978  brab  3979  opelopabaf  3980  unex  4122  snnex  4127  op1stb  4155  onun2i  4163  onsucsssucexmid  4192  onsucelsucexmid  4195  opthreg  4214  tfis  4229  finds  4246  finds2  4247  nnregexmid  4265  xpeq12i  4290  opelvv  4313  eqrelriiv  4357  eqrelrdv  4359  relsnop  4367  xpss  4369  xpex  4376  relop  4409  brco  4429  opelcnv  4440  brcnv  4441  asymref  4633  codir  4636  ssrnres  4686  dmprop  4718  op2ndb  4727  dfco2  4743  cossxp  4766  coex  4786  funsn  4870  fnsn  4875  feq23i  4963  resasplitss  4990  fabex  4999  fvex  5116  xpsn  5260  fmptap  5274  fvsn  5279  opabex  5306  acexmidlemv  5430  oveq12i  5444  oprabid  5457  oprabss  5509  caovcom  5577  opabex3  5668  iunex  5669  oprabex  5674  ofmres  5682  op1st  5692  op2nd  5693  fo1st  5703  fo2nd  5704  mpt2ex  5755  1stconst  5761  2ndconst  5762  algrflem  5769  dftpos4  5796  tpostpos  5797  tpossym  5809  rdgruledef  5890  rdg0  5891  frecfnom  5897  sucinc  5936  fnoei  5943  oeiexg  5944  nnacli  5972  nnmcli  5973  elec  6052  ecovcom  6120  ecovass  6122  ecovdi  6124  1lt2pi  6194  1nq  6219  rec1nq  6248  1lt2nq  6258  ltaddnq  6259  halfnqq  6261  prarloclemarch2  6270  prarloclemlt  6341  prarloclemcalc  6350  genpelxp  6359  genpelpw  6365  ltexprlempr  6439  recexprlempr  6460  0r  6491  1sr  6492  m1r  6493  m1p1sr  6501  m1m1sr  6502  0lt1sr  6506  1ne0sr  6507  1idsr  6509  recexsrlem  6514  axi2m1  6563  axprecex  6568  axcnre  6569  0cn  6615  addcli  6627  mulcli  6628  mulcomi  6629  readdcli  6636  remulcli  6637  rexpssxrxp  6665  ltrelxr  6675  gtneii  6705  ltnsymi  6707  lenlti  6708  ltlei  6709  mulgt0i  6716  mulgt0ii  6717  0lt1  6728  addcomi  6744  pncan3oi  6814  resubcli  6860  subcli  6873  pncan3i  6874  negsubi  6875  subnegi  6876  subeq0i  6877  neg11i  6878  negcon1i  6879  negcon2i  6880  mulneg1i  6987  mulneg2i  6988  mul2negi  6989  addgt0ii  7066  ltnegi  7067  lenegi  7068  ltnegcon2i  7069  ltaddposi  7070  posdifi  7071  ltnegcon1i  7072  lenegcon1i  7073  subge0i  7074  bj-unex  7281  bj-nn0suc0  7311  bj-nntrans  7312  bj-nnelirr  7314
  Copyright terms: Public domain W3C validator