ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpd Structured version   Unicode 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  6500  genpmu  6501  genprndl  6504  genprndu  6505  genpdisj  6506  addnqprllem  6510  addnqprulem  6511  addlocprlemeq  6516  addlocprlemgt  6517  addlocprlem  6518  addlocpr  6519  nqprloc  6528  addnqpr1lemrl  6537  addnqpr1lemru  6538  appdivnq  6542  prmuloc  6545  prmuloc2  6546  mullocprlem  6549  mullocpr  6550  ltprordil  6563  ltpopr  6567  ltsopr  6568  ltaddpr  6569  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemlol  6574  ltexprlemopu  6575  ltexprlemupu  6576  ltexprlemloc  6579  ltexprlemfl  6581  ltexprlemrl  6582  ltexprlemfu  6583  ltexprlemru  6584  ltaprg  6590  recexprlemm  6594  recexprlem1ssl  6603  recexprlem1ssu  6604  aptiprleml  6609  aptiprlemu  6610  archpr  6613  recexgt0sr  6661  mulgt0sr  6664  archsr  6668  axarch  6733  lelttr  6863  ltletr  6864  ltled  6892  cnegexlem1  6943  cnegexlem2  6944  renegcl  7028  gt0add  7317  apreap  7331  apirr  7349  apsym  7350  apcotr  7351  apadd1  7352  apneg  7355  mulext1  7356  mulap0r  7359  apti  7366  recexap  7376  mulap0  7377  receuap  7392  lep1  7552  lem1  7554  letrp1  7555  recreclt  7607  nnrecgt0  7692  bndndx  7916  nn0ge2m1nn  7978  elnn0z  7994  peano2z  8017  zaddcl  8021  ztri3or0  8023  zltnle  8027  zdceq  8052  zdcle  8053  zdclt  8054  zdiv  8064  zeo  8079  fnn0ind  8090  btwnz  8093  uzm1  8239  uzp1  8242  indstr  8272  eluzdc  8283  nn01to3  8288  qapne  8310  xrlelttr  8452  xrltletr  8453  ge0nemnf  8467  fzdcel  8634  elfzouz2  8747  fzoss1  8757  fzospliti  8762  fzocatel  8785  fzostep1  8823  frec2uzzd  8827  frec2uzuzd  8829  frec2uzlt2d  8831  frec2uzf1od  8833  frecuzrdgrrn  8835  frecuzrdgcl  8840  frecuzrdgsuc  8842  iseqval  8860  iseqfveq2  8865  expgt1  8907  expnbnd  8985  expnlbnd2  8987  cjap  9094  bj-exlimmpi  9179  bj-2inf  9326  bj-peano4  9343  bj-nn0suc  9348
  Copyright terms: Public domain W3C validator