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  6410  mulclpi  6424  nlt1pig  6437  indpi  6438  recclnq  6488  ltexnqq  6504  halfnqq  6506  prarloclemarch  6514  prarloclemarch2  6515  prop  6571  prltlu  6583  prarloclem3step  6592  prarloclem5  6596  prarloclem  6597  prarloc  6599  prarloc2  6600  genpml  6613  genpmu  6614  genprndl  6617  genprndu  6618  genpdisj  6619  addnqprllem  6623  addnqprulem  6624  addlocprlemeq  6629  addlocprlemgt  6630  addlocprlem  6631  addlocpr  6632  nqprloc  6641  nqprl  6647  nqpru  6648  addnqprlemrl  6653  addnqprlemru  6654  appdivnq  6659  prmuloc  6662  prmuloc2  6663  mullocprlem  6666  mullocpr  6667  mulnqprlemrl  6669  mulnqprlemru  6670  ltprordil  6685  ltpopr  6691  ltsopr  6692  ltaddpr  6693  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemlol  6698  ltexprlemopu  6699  ltexprlemupu  6700  ltexprlemloc  6703  ltexprlemfl  6705  ltexprlemrl  6706  ltexprlemfu  6707  ltexprlemru  6708  ltaprg  6715  recexprlemm  6720  recexprlem1ssl  6729  recexprlem1ssu  6730  aptiprleml  6735  aptiprlemu  6736  archpr  6739  cauappcvgprlemm  6741  cauappcvgprlemopl  6742  cauappcvgprlemlol  6743  cauappcvgprlemopu  6744  cauappcvgprlemupu  6745  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  cauappcvgprlemladdru  6752  cauappcvgprlem1  6755  archrecpr  6760  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemm  6764  caucvgprlemopl  6765  caucvgprlemlol  6766  caucvgprlemopu  6767  caucvgprlemupu  6768  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprlemladdfu  6773  caucvgprlem1  6775  caucvgprlemlim  6777  caucvgprprlemnbj  6789  caucvgprprlemml  6790  caucvgprprlemopl  6793  caucvgprprlemlol  6794  caucvgprprlemopu  6795  caucvgprprlemupu  6796  caucvgprprlemdisj  6798  caucvgprprlemloc  6799  caucvgprprlemexbt  6802  caucvgprprlemaddq  6804  caucvgprprlemlim  6807  recexgt0sr  6856  mulgt0sr  6860  archsr  6864  caucvgsrlemoffcau  6880  axarch  6963  axcaucvglemcau  6970  lelttr  7104  ltletr  7105  ltled  7133  cnegexlem1  7184  cnegexlem2  7185  renegcl  7270  gt0add  7562  apreap  7576  apirr  7594  apsym  7595  apcotr  7596  apadd1  7597  apneg  7600  mulext1  7601  mulap0r  7604  apti  7611  recexap  7632  mulap0  7633  receuap  7648  lep1  7809  lem1  7811  letrp1  7812  recreclt  7864  nnrecgt0  7949  bndndx  8178  nn0ge2m1nn  8240  elnn0z  8256  peano2z  8279  zaddcl  8283  ztri3or0  8285  zltnle  8289  zdceq  8314  zdcle  8315  zdclt  8316  zdiv  8326  zeo  8341  fnn0ind  8352  btwnz  8355  uzm1  8501  uzp1  8504  indstr  8534  eluzdc  8545  nn01to3  8550  qapne  8572  xrlelttr  8720  xrltletr  8721  ge0nemnf  8735  fzdcel  8902  elfzouz2  9015  fzoss1  9025  fzospliti  9030  fzocatel  9053  fzostep1  9091  qtri3or  9096  qltnle  9099  qdceq  9100  qbtwnzlemex  9103  rebtwn2zlemstep  9105  rebtwn2z  9107  flqeqceilz  9158  frec2uzzd  9160  frec2uzuzd  9162  frec2uzlt2d  9164  frec2uzf1od  9166  frecuzrdgrrn  9168  frecuzrdgcl  9173  frecuzrdgsuc  9175  iseqval  9194  iseqss  9200  iseqfveq2  9202  iseqshft2  9206  monoord  9209  iseqsplit  9212  iseqcaopr3  9214  iseqid3s  9220  iseqhomo  9222  expgt1  9267  expnbnd  9346  expnlbnd2  9348  cjap  9480  caucvgre  9554  cvg1nlemres  9558  resqrexlemgt0  9592  resqrexlemglsq  9594  resqrexlemga  9595  resqrtcl  9601  abslt  9658  abssubap0  9660  abssubne0  9661  caubnd2  9687  qdenre  9772  climuni  9788  2clim  9796  climcn1  9803  climcn2  9804  subcn2  9806  mulcn2  9807  climsqz  9829  climsqz2  9830  climcau  9840  climcvg1nlem  9842  climcaucn  9844  serif0  9845  sqrt2irr  9852  ialgcvga  9864  ialgfx  9865  bj-exlimmpi  9884  bj-2inf  10036  bj-peano4  10054  bj-nn0suc  10063
  Copyright terms: Public domain W3C validator