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

Theorem mpd 13
Description: A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpd.1  |-  ( ph  ->  ps )
mpd.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mpd  |-  ( ph  ->  ch )

Proof of Theorem mpd
StepHypRef Expression
1 mpd.1 . 2  |-  ( ph  ->  ps )
2 mpd.2 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
32a2i 11 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
41, 3ax-mp 7 1  |-  ( ph  ->  ch )
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  638  impidc  755  jadc  760  pm2.54dc  790  stabtestimpdc  824  pm4.55dc  846  oplem1  882  xor3dc  1278  exlimdd  1752  exlimddv  1778  eqrdav  2039  necon1aidc  2256  necon1bidc  2257  necon4aidc  2273  rexlimddv  2437  vtoclgft  2604  sseldd  2946  ssneldd  2948  tpid3g  3483  preq12b  3541  axpweq  3924  opth  3974  issod  4056  frirrg  4087  frind  4089  ralxfr2d  4196  rexxfr2d  4197  eldifpw  4208  onun2  4216  onuni  4220  elirr  4266  en2lp  4278  wetriext  4301  peano2  4318  relop  4486  elres  4646  sotri2  4722  iota4an  4886  iota5  4887  funeu  4926  funopg  4934  imadiflem  4978  funimaexglem  4982  ssimaex  5234  ffvelrn  5300  dff3im  5312  dffo4  5315  f1eqcocnv  5431  f1oiso2  5466  riota5f  5492  riotass2  5494  acexmidlemcase  5507  ovmpt2df  5632  ovmpt2dv2  5634  ovi3  5637  ov6g  5638  caoftrn  5736  op1steq  5805  tfr0  5937  tfrlemibxssdm  5941  tfrlemi14d  5947  rdgivallem  5968  frecsuclem3  5990  freccl  5993  nnsucelsuc  6070  nnsucsssuc  6071  nnawordex  6101  ersym  6118  fundmen  6286  fidceq  6330  fin0or  6343  findcard2  6346  findcard2s  6347  elni2  6412  mulclpi  6426  nlt1pig  6439  indpi  6440  recclnq  6490  ltexnqq  6506  halfnqq  6508  prarloclemarch  6516  prarloclemarch2  6517  prop  6573  prltlu  6585  prarloclem3step  6594  prarloclem5  6598  prarloclem  6599  prarloc  6601  prarloc2  6602  genpml  6615  genpmu  6616  genprndl  6619  genprndu  6620  genpdisj  6621  addnqprllem  6625  addnqprulem  6626  addlocprlemeq  6631  addlocprlemgt  6632  addlocprlem  6633  addlocpr  6634  nqprloc  6643  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  appdivnq  6661  prmuloc  6664  prmuloc2  6665  mullocprlem  6668  mullocpr  6669  mulnqprlemrl  6671  mulnqprlemru  6672  ltprordil  6687  ltpopr  6693  ltsopr  6694  ltaddpr  6695  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemloc  6705  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  ltaprg  6717  recexprlemm  6722  recexprlem1ssl  6731  recexprlem1ssu  6732  aptiprleml  6737  aptiprlemu  6738  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemupu  6747  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlem1  6757  archrecpr  6762  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemupu  6770  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlem1  6777  caucvgprlemlim  6779  caucvgprprlemnbj  6791  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemupu  6798  caucvgprprlemdisj  6800  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemaddq  6806  caucvgprprlemlim  6809  recexgt0sr  6858  mulgt0sr  6862  archsr  6866  caucvgsrlemoffcau  6882  axarch  6965  axcaucvglemcau  6972  lelttr  7106  ltletr  7107  ltled  7135  cnegexlem1  7186  cnegexlem2  7187  renegcl  7272  gt0add  7564  apreap  7578  apirr  7596  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  mulap0r  7606  apti  7613  recexap  7634  mulap0  7635  receuap  7650  lep1  7811  lem1  7813  letrp1  7814  recreclt  7866  nnrecgt0  7951  bndndx  8180  nn0ge2m1nn  8242  elnn0z  8258  peano2z  8281  zaddcl  8285  ztri3or0  8287  zltnle  8291  zdceq  8316  zdcle  8317  zdclt  8318  zdiv  8328  zeo  8343  fnn0ind  8354  btwnz  8357  uzm1  8503  uzp1  8506  indstr  8536  eluzdc  8547  nn01to3  8552  qapne  8574  xrlelttr  8722  xrltletr  8723  ge0nemnf  8737  fzdcel  8904  elfzouz2  9017  fzoss1  9027  fzospliti  9032  fzocatel  9055  fzostep1  9093  qtri3or  9098  qltnle  9101  qdceq  9102  qbtwnzlemex  9105  rebtwn2zlemstep  9107  rebtwn2z  9109  flqeqceilz  9160  frec2uzzd  9186  frec2uzuzd  9188  frec2uzlt2d  9190  frec2uzf1od  9192  frecuzrdgrrn  9194  frecuzrdgcl  9199  frecuzrdgsuc  9201  iseqval  9220  iseqss  9226  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  iseqcaopr3  9240  iseqid3s  9246  iseqhomo  9248  expgt1  9293  expnbnd  9372  expnlbnd2  9374  cjap  9506  caucvgre  9580  cvg1nlemres  9584  resqrexlemgt0  9618  resqrexlemglsq  9620  resqrexlemga  9621  resqrtcl  9627  abslt  9684  abssubap0  9686  abssubne0  9687  caubnd2  9713  qdenre  9798  climuni  9814  2clim  9822  climcn1  9829  climcn2  9830  subcn2  9832  mulcn2  9833  climsqz  9855  climsqz2  9856  climcau  9866  climcvg1nlem  9868  climcaucn  9870  serif0  9871  sqrt2irr  9878  ialgcvga  9890  ialgfx  9891  bj-exlimmpi  9910  bj-2inf  10062  bj-peano4  10080  bj-nn0suc  10089
  Copyright terms: Public domain W3C validator