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  411  pm2.21dd  538  mt2d  543  mpjaod  625  impidc  743  jadc  748  pm2.54dc  778  stabtestimpdc  812  pm4.55dc  832  oplem1  868  xor3dc  1259  exlimdd  1730  exlimddv  1756  eqrdav  2017  necon1aidc  2230  necon1bidc  2231  necon4aidc  2247  rexlimddv  2411  vtoclgft  2577  sseldd  2919  ssneldd  2921  tpid3g  3453  preq12b  3511  axpweq  3894  opth  3944  issod  4026  ralxfr2d  4142  rexxfr2d  4143  eldifpw  4154  onun2  4162  onuni  4166  elirr  4204  en2lp  4212  peano2  4241  relop  4409  elres  4569  sotri2  4645  iota4an  4809  iota5  4810  funeu  4848  funopg  4856  imadiflem  4900  funimaexglem  4904  ssimaex  5155  ffvelrn  5221  dff3im  5233  dffo4  5236  f1eqcocnv  5352  f1oiso2  5387  riota5f  5412  riotass2  5414  acexmidlemcase  5427  ovmpt2df  5551  ovmpt2dv2  5553  ovi3  5556  ov6g  5557  caoftrn  5655  op1steq  5724  tfrlemibxssdm  5858  tfrlemi14d  5864  rdgivallem  5884  frec0g  5898  frecsuclem3  5902  nnsucelsuc  5981  nnsucsssuc  5982  nnawordex  6008  ersym  6025  elni2  6168  mulclpi  6182  nlt1pig  6195  recclnq  6245  ltexnqq  6260  halfnqq  6261  prarloclemarch  6269  prarloclemarch2  6270  prop  6323  prltlu  6335  prnmaddl  6338  prarloclem3step  6344  prarloclem5  6348  prarloclem  6349  prarloc  6351  prarloc2  6352  genpml  6366  genpmu  6367  genprndl  6370  genprndu  6371  genpdisj  6372  addnqprllem  6376  addnqprulem  6377  addlocprlemeq  6382  addlocprlemgt  6383  addlocprlem  6384  addlocpr  6385  nqprloc  6394  appdivnq  6401  prmuloc  6404  prmuloc2  6405  mullocprlem  6408  mullocpr  6409  ltprordil  6422  ltpopr  6426  ltsopr  6427  ltaddpr  6428  ltexprlemm  6431  ltexprlemopl  6432  ltexprlemlol  6433  ltexprlemopu  6434  ltexprlemupu  6435  ltexprlemloc  6438  ltexprlemfl  6440  ltexprlemrl  6441  ltexprlemfu  6442  ltexprlemru  6443  addcanprleml  6445  ltaprg  6449  recexprlemm  6452  recexprlem1ssl  6461  recexprlem1ssu  6462  recexsrlem  6514  mulgt0sr  6516  lelttr  6698  ltletr  6699  ltled  6722  cnegexlem1  6773  cnegexlem2  6774  renegcl  6858  bj-exlimmpi  7156  bj-2inf  7299  bj-peano4  7316  bj-nn0suc  7321
  Copyright terms: Public domain W3C validator