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 5 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-2 7
This theorem is referenced by:  syl  14  mpi  15  id  19  mpcom  36  mpdd  41  mp2d  47  pm2.43i  49  syl3c  63  mpbid  146  mpbird  166  jcai  309  mp2and  430  pm2.21dd  610  mt2d  615  mpjaod  708  stdcndcOLD  832  impidc  844  jadc  849  pm2.54dc  877  pm4.55dc  923  oplem1  960  mp3and  1319  xor3dc  1366  exlimdd  1845  exlimddv  1871  eqrdav  2139  necon1aidc  2360  necon1bidc  2361  necon4aidc  2377  reximddv  2538  reximssdv  2539  rexlimddv  2557  vtoclgft  2739  rspcedvd  2798  sseldd  3101  ssneldd  3103  tpid3g  3644  preq12b  3703  axpweq  4101  exmid1dc  4129  opth  4165  issod  4247  frirrg  4278  frind  4280  ralxfr2d  4391  rexxfr2d  4392  eldifpw  4404  onun2  4412  onuni  4416  elirr  4462  en2lp  4475  wetriext  4497  peano2  4515  relop  4695  elres  4861  sotri2  4942  iota4an  5113  iota5  5114  funeu  5154  funopg  5163  imadiflem  5208  funimaexglem  5212  ssimaex  5488  ffvelrn  5559  dff3im  5571  dffo4  5574  f1eqcocnv  5698  f1oiso2  5734  riota5f  5760  riotass2  5762  acexmidlemcase  5775  ovmpodf  5908  ovmpodv2  5910  ovi3  5913  ov6g  5914  caoftrn  6013  op1steq  6083  tfr0dm  6225  tfrlemibxssdm  6230  tfrlemi14d  6236  tfr1onlembxssdm  6246  tfr1onlemaccex  6251  tfr1onlemres  6252  tfrcllembxssdm  6259  tfrcllemaccex  6264  tfrcllemres  6265  rdgivallem  6284  nnsucelsuc  6393  nnsucsssuc  6394  dcdifsnid  6406  nnawordex  6430  ersym  6447  mapvalg  6558  pmvalg  6559  mapsn  6590  fundmen  6706  mapdom1g  6747  fidceq  6769  fin0or  6786  findcard2  6789  findcard2s  6790  fiintim  6823  suplub2ti  6894  supsnti  6898  supisoex  6902  difinfsnlem  6990  difinfsn  6991  ctm  7000  ctssdclemn0  7001  ctssdccl  7002  ctssdc  7004  enumctlemm  7005  enomnilem  7016  exmidomniim  7019  exmidomni  7020  fodjuomnilemdc  7022  fodjuomnilemres  7026  omnimkv  7036  mkvprop  7038  omniwomnimkv  7047  en2eleq  7066  acfun  7078  ccfunen  7094  cc4f  7099  cc4n  7101  elni2  7144  mulclpi  7158  nlt1pig  7171  indpi  7172  recclnq  7222  ltexnqq  7238  halfnqq  7240  prarloclemarch  7248  prarloclemarch2  7249  prop  7305  prltlu  7317  prarloclem3step  7326  prarloclem5  7330  prarloclem  7331  prarloc  7333  prarloc2  7334  genpml  7347  genpmu  7348  genprndl  7351  genprndu  7352  genpdisj  7353  addnqprllem  7357  addnqprulem  7358  addlocprlemeq  7363  addlocprlemgt  7364  addlocprlem  7365  addlocpr  7366  nqprloc  7375  nqprl  7381  nqpru  7382  addnqprlemrl  7387  addnqprlemru  7388  appdivnq  7393  prmuloc  7396  prmuloc2  7397  mullocprlem  7400  mullocpr  7401  mulnqprlemrl  7403  mulnqprlemru  7404  ltprordil  7419  ltpopr  7425  ltsopr  7426  ltaddpr  7427  ltexprlemm  7430  ltexprlemopl  7431  ltexprlemlol  7432  ltexprlemopu  7433  ltexprlemupu  7434  ltexprlemloc  7437  ltexprlemfl  7439  ltexprlemrl  7440  ltexprlemfu  7441  ltexprlemru  7442  ltaprg  7449  recexprlemm  7454  recexprlem1ssl  7463  recexprlem1ssu  7464  aptiprleml  7469  aptiprlemu  7470  archpr  7473  cauappcvgprlemm  7475  cauappcvgprlemopl  7476  cauappcvgprlemlol  7477  cauappcvgprlemopu  7478  cauappcvgprlemupu  7479  cauappcvgprlemdisj  7481  cauappcvgprlemloc  7482  cauappcvgprlemladdfu  7484  cauappcvgprlemladdfl  7485  cauappcvgprlemladdru  7486  cauappcvgprlem1  7489  archrecpr  7494  caucvgprlemnkj  7496  caucvgprlemnbj  7497  caucvgprlemm  7498  caucvgprlemopl  7499  caucvgprlemlol  7500  caucvgprlemopu  7501  caucvgprlemupu  7502  caucvgprlemdisj  7504  caucvgprlemloc  7505  caucvgprlemladdfu  7507  caucvgprlem1  7509  caucvgprlemlim  7511  caucvgprprlemnbj  7523  caucvgprprlemml  7524  caucvgprprlemopl  7527  caucvgprprlemlol  7528  caucvgprprlemopu  7529  caucvgprprlemupu  7530  caucvgprprlemdisj  7532  caucvgprprlemloc  7533  caucvgprprlemexbt  7536  caucvgprprlemaddq  7538  caucvgprprlemlim  7541  suplocexprlemss  7545  suplocexprlemrl  7547  suplocexprlemmu  7548  suplocexprlemru  7549  suplocexprlemdisj  7550  suplocexprlemloc  7551  suplocexprlemub  7553  suplocexprlemlub  7554  recexgt0sr  7603  mulgt0sr  7608  archsr  7612  caucvgsrlemoffcau  7628  suplocsrlemb  7636  suplocsrlempr  7637  suplocsrlem  7638  cnm  7662  axarch  7721  axcaucvglemcau  7728  axpre-suploclemres  7731  lelttr  7874  ltletr  7875  ltled  7903  cnegexlem1  7959  cnegexlem2  7960  renegcl  8045  negf1o  8166  gt0add  8357  apreap  8371  apirr  8389  apsym  8390  apcotr  8391  apadd1  8392  apneg  8395  mulext1  8396  mulap0r  8399  apti  8406  aprcl  8430  recexap  8436  mulap0  8437  receuap  8452  mul0eqap  8453  lep1  8625  lem1  8627  letrp1  8628  recreclt  8680  lbinf  8728  suprubex  8731  nnrecgt0  8780  bndndx  8998  nn0ge2m1nn  9059  elnn0z  9089  peano2z  9112  zaddcl  9116  ztri3or0  9118  zltnle  9122  zdceq  9148  zdcle  9149  zdclt  9150  zdiv  9161  zeo  9178  fnn0ind  9189  btwnz  9192  uzm1  9378  uzp1  9381  indstr  9413  supinfneg  9415  infsupneg  9416  eluzdc  9429  nn01to3  9434  qapne  9456  xrltled  9613  xrlelttr  9617  xrltletr  9618  ge0nemnf  9635  fzdcel  9849  elfzouz2  9967  fzoss1  9977  fzospliti  9982  fzocatel  10005  fzostep1  10043  qtri3or  10049  qltnle  10052  qdceq  10053  exbtwnzlemex  10056  rebtwn2zlemstep  10059  rebtwn2z  10061  qbtwnxr  10064  ioom  10067  ico0  10068  ioc0  10069  flqeqceilz  10120  modqadd1  10163  modqmul1  10179  frec2uzuzd  10204  frec2uzlt2d  10206  frec2uzf1od  10208  frecuzrdgrrn  10210  frec2uzrdg  10211  frecuzrdgrcl  10212  frecuzrdgsuc  10216  frecuzrdgrclt  10217  frecuzrdgdomlem  10219  uzsinds  10244  seqvalcd  10261  seqovcd  10265  seq3fveq2  10271  seq3shft2  10275  monoord  10278  seq3split  10281  seq3caopr3  10283  iseqf1olemab  10291  iseqf1olemnanb  10292  iseqf1olemqk  10296  seq3id3  10309  seq3id2  10311  seq3homo  10312  expgt1  10360  m1expeven  10369  expnbnd  10444  expnlbnd2  10446  apexp1  10494  hashennn  10556  zfz1isolem1  10613  seq3coll  10615  cjap  10708  caucvgre  10783  cvg1nlemres  10787  resqrexlemgt0  10822  resqrexlemglsq  10824  resqrexlemga  10825  resqrtcl  10831  abslt  10890  abssubap0  10892  abssubne0  10893  caubnd2  10919  qdenre  11004  maxabslemlub  11009  maxabs  11011  maxleast  11015  fimaxre2  11028  xrmaxiflemlub  11047  xrmaxif  11050  xrmaxltsup  11057  xrmaxadd  11060  xrmineqinf  11068  climuni  11092  2clim  11100  climcn1  11107  climcn2  11108  subcn2  11110  mulcn2  11111  climsqz  11134  climsqz2  11135  climcau  11146  climcvg1nlem  11148  climcaucn  11150  serf0  11151  sumrbdclem  11176  summodclem2  11181  zsumdc  11183  divcnv  11296  absltap  11308  absgtap  11309  mertenslem2  11335  ntrivcvgap  11347  prodrbdclem  11370  prodmodclem2  11376  efcllemp  11394  tanvalap  11444  sin01bnd  11493  cos01bnd  11494  sin01gt0  11497  absef  11505  eirrap  11513  dvds0  11537  dvdsmul1  11544  dvdsmultr1d  11561  dvdslelemd  11570  divconjdvds  11576  alzdvds  11581  sqoddm1div8z  11612  nno  11632  divalglemex  11648  zsupcllemstep  11667  zsupcl  11669  infssuzledc  11672  dvdsbnd  11674  dvdslegcd  11682  zeqzmulgcd  11688  gcd0id  11696  gcdaddm  11701  gcd1  11704  gcdabs  11705  bezoutlemnewy  11713  bezoutlemstep  11714  bezoutlemmain  11715  bezoutlemex  11718  bezoutlemzz  11719  bezoutlemaz  11720  bezoutlembz  11721  bezoutlembi  11722  bezoutlemle  11725  bezoutlemsup  11726  mulgcd  11733  gcdzeq  11739  dvdsmulgcd  11742  sqgcd  11746  bezoutr1  11750  algcvga  11761  algfx  11762  eucalglt  11767  eucalg  11769  lcmneg  11784  lcmabs  11786  lcmgcdlem  11787  ncoprmgcdne1b  11799  mulgcddvds  11804  qredeq  11806  divgcdcoprm0  11811  cncongr1  11813  isprm2lem  11826  nprm  11833  dvdsnprmd  11835  prmdvdsfz  11848  coprm  11851  isprm6  11854  sqrt2irr  11869  pw2dvdslemn  11872  pw2dvdseulemle  11874  oddpwdclemdvds  11877  oddpwdclemndvds  11878  sqrt2irrap  11887  qnumdencl  11894  ennnfonelemex  11956  ennnfonelemhom  11957  ennnfonelemrnh  11958  ennnfonelemnn0  11964  ennnfonelemim  11966  exmidunben  11968  ctinfomlemom  11969  ctinfom  11970  ctinf  11972  omctfn  11985  tgcl  12265  neii1  12348  neii2  12350  neiss  12351  tpnei  12361  tgrest  12370  ssrest  12383  icnpimaex  12412  lmcvg  12418  cnpnei  12420  cnptopco  12423  lmff  12450  txcnp  12472  txcn  12476  hmeontr  12514  blssec  12639  mopni3  12685  blsscls2  12694  comet  12700  bdxmet  12702  bdmopn  12705  xmettxlem  12710  xmettx  12711  addcncntoplem  12752  mulc1cncf  12777  cncfco  12779  cncfmptc  12783  mulcncflem  12791  mulcncf  12792  dedekindeulemlu  12800  dedekindeulemeu  12801  suplociccreex  12803  suplociccex  12804  dedekindicclemlu  12809  dedekindicclemeu  12810  ivthinclemlopn  12815  ivthinclemlr  12816  ivthinclemuopn  12817  ivthinclemur  12818  ivthinclemloc  12820  ivthinc  12822  limcimolemlt  12834  limcresi  12836  cnplimcim  12837  cnplimclemle  12838  cnplimclemr  12839  limccnpcntop  12845  limccoap  12848  dvcoapbr  12872  dvcj  12874  efltlemlt  12896  sin0pilem2  12904  tangtx  12960  logdivlti  13003  rplogbval  13063  logbgcd1irraplemexp  13086  logbgcd1irraplemap  13087  logbgcd1irrap  13088  bj-exlimmpi  13141  uzdcinzz  13169  bj-2inf  13300  bj-peano4  13317  bj-nn0suc  13326  exmid1stab  13361  subctctexmid  13362  nninfalllem1  13371  nninfsellemqall  13379  nninfomnilem  13382  nninffeq  13384  exmidsbthrlem  13385  sbthomlem  13388  refeq  13391  isomninnlem  13393  apdifflemr  13408  redcwlpo  13415
  Copyright terms: Public domain W3C validator