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

Theorem mpd 13
Description: A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpd.1 (φψ)
mpd.2 (φ → (ψχ))
Assertion
Ref Expression
mpd (φχ)

Proof of Theorem mpd
StepHypRef Expression
1 mpd.1 . 2 (φψ)
2 mpd.2 . . 3 (φ → (ψχ))
32a2i 11 . 2 ((φψ) → (φχ))
41, 3ax-mp 7 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-2 6  ax-mp 7
This theorem is referenced by:  syl  14  mpi  15  id  19  mpcom  32  mpdd  36  mp2d  41  pm2.43i  43  syl3c  57  mpbid  135  mpbird  156  jcai  294  mp2and  409  pm2.21dd  550  mt2d  555  mpjaod  637  impidc  754  jadc  759  pm2.54dc  789  stabtestimpdc  823  pm4.55dc  845  oplem1  881  xor3dc  1275  exlimdd  1749  exlimddv  1775  eqrdav  2036  necon1aidc  2250  necon1bidc  2251  necon4aidc  2267  rexlimddv  2431  vtoclgft  2598  sseldd  2940  ssneldd  2942  tpid3g  3474  preq12b  3532  axpweq  3915  opth  3965  issod  4047  ralxfr2d  4162  rexxfr2d  4163  eldifpw  4174  onun2  4182  onuni  4186  elirr  4224  en2lp  4232  peano2  4261  relop  4429  elres  4589  sotri2  4665  iota4an  4829  iota5  4830  funeu  4869  funopg  4877  imadiflem  4921  funimaexglem  4925  ssimaex  5177  ffvelrn  5243  dff3im  5255  dffo4  5258  f1eqcocnv  5374  f1oiso2  5409  riota5f  5435  riotass2  5437  acexmidlemcase  5450  ovmpt2df  5574  ovmpt2dv2  5576  ovi3  5579  ov6g  5580  caoftrn  5678  op1steq  5747  tfr0  5878  tfrlemibxssdm  5882  tfrlemi14d  5888  rdgivallem  5908  frecsuclem3  5929  freccl  5932  nnsucelsuc  6009  nnsucsssuc  6010  nnawordex  6037  ersym  6054  fundmen  6222  elni2  6298  mulclpi  6312  nlt1pig  6325  indpi  6326  recclnq  6376  ltexnqq  6391  halfnqq  6393  prarloclemarch  6401  prarloclemarch2  6402  prop  6457  prltlu  6469  prarloclem3step  6478  prarloclem5  6482  prarloclem  6483  prarloc  6485  prarloc2  6486  genpml  6499  genpmu  6500  genprndl  6503  genprndu  6504  genpdisj  6505  addnqprllem  6509  addnqprulem  6510  addlocprlemeq  6515  addlocprlemgt  6516  addlocprlem  6517  addlocpr  6518  nqprloc  6527  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  appdivnq  6543  prmuloc  6546  prmuloc2  6547  mullocprlem  6550  mullocpr  6551  ltprordil  6564  ltpopr  6568  ltsopr  6569  ltaddpr  6570  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemlol  6575  ltexprlemopu  6576  ltexprlemupu  6577  ltexprlemloc  6580  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  ltaprg  6591  recexprlemm  6595  recexprlem1ssl  6604  recexprlem1ssu  6605  aptiprleml  6610  aptiprlemu  6611  archpr  6614  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemopu  6619  cauappcvgprlemupu  6620  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlem1  6630  recexgt0sr  6681  mulgt0sr  6684  archsr  6688  axarch  6753  lelttr  6883  ltletr  6884  ltled  6912  cnegexlem1  6963  cnegexlem2  6964  renegcl  7048  gt0add  7337  apreap  7351  apirr  7369  apsym  7370  apcotr  7371  apadd1  7372  apneg  7375  mulext1  7376  mulap0r  7379  apti  7386  recexap  7396  mulap0  7397  receuap  7412  lep1  7572  lem1  7574  letrp1  7575  recreclt  7627  nnrecgt0  7712  bndndx  7936  nn0ge2m1nn  7998  elnn0z  8014  peano2z  8037  zaddcl  8041  ztri3or0  8043  zltnle  8047  zdceq  8072  zdcle  8073  zdclt  8074  zdiv  8084  zeo  8099  fnn0ind  8110  btwnz  8113  uzm1  8259  uzp1  8262  indstr  8292  eluzdc  8303  nn01to3  8308  qapne  8330  xrlelttr  8472  xrltletr  8473  ge0nemnf  8487  fzdcel  8654  elfzouz2  8767  fzoss1  8777  fzospliti  8782  fzocatel  8805  fzostep1  8843  frec2uzzd  8847  frec2uzuzd  8849  frec2uzlt2d  8851  frec2uzf1od  8853  frecuzrdgrrn  8855  frecuzrdgcl  8860  frecuzrdgsuc  8862  iseqval  8880  iseqfveq2  8885  expgt1  8927  expnbnd  9005  expnlbnd2  9007  cjap  9114  bj-exlimmpi  9225  bj-2inf  9372  bj-peano4  9389  bj-nn0suc  9394
  Copyright terms: Public domain W3C validator