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  429  pm2.21dd  594  mt2d  599  mpjaod  692  stdcndcOLD  816  impidc  828  jadc  833  pm2.54dc  861  pm4.55dc  907  oplem1  944  mp3and  1303  xor3dc  1350  exlimdd  1828  exlimddv  1854  eqrdav  2116  necon1aidc  2336  necon1bidc  2337  necon4aidc  2353  reximddv  2512  reximssdv  2513  rexlimddv  2531  vtoclgft  2710  rspcedvd  2769  sseldd  3068  ssneldd  3070  tpid3g  3608  preq12b  3667  axpweq  4065  exmid1dc  4093  opth  4129  issod  4211  frirrg  4242  frind  4244  ralxfr2d  4355  rexxfr2d  4356  eldifpw  4368  onun2  4376  onuni  4380  elirr  4426  en2lp  4439  wetriext  4461  peano2  4479  relop  4659  elres  4825  sotri2  4906  iota4an  5077  iota5  5078  funeu  5118  funopg  5127  imadiflem  5172  funimaexglem  5176  ssimaex  5450  ffvelrn  5521  dff3im  5533  dffo4  5536  f1eqcocnv  5660  f1oiso2  5696  riota5f  5722  riotass2  5724  acexmidlemcase  5737  ovmpodf  5870  ovmpodv2  5872  ovi3  5875  ov6g  5876  caoftrn  5975  op1steq  6045  tfr0dm  6187  tfrlemibxssdm  6192  tfrlemi14d  6198  tfr1onlembxssdm  6208  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllembxssdm  6221  tfrcllemaccex  6226  tfrcllemres  6227  rdgivallem  6246  nnsucelsuc  6355  nnsucsssuc  6356  dcdifsnid  6368  nnawordex  6392  ersym  6409  mapvalg  6520  pmvalg  6521  mapsn  6552  fundmen  6668  mapdom1g  6709  fidceq  6731  fin0or  6748  findcard2  6751  findcard2s  6752  fiintim  6785  suplub2ti  6856  supsnti  6860  supisoex  6864  difinfsnlem  6952  difinfsn  6953  ctm  6962  ctssdclemn0  6963  ctssdccl  6964  ctssdc  6966  enumctlemm  6967  enomnilem  6978  exmidomniim  6981  exmidomni  6982  fodjuomnilemdc  6984  fodjuomnilemres  6988  omnimkv  6998  mkvprop  7000  en2eleq  7019  acfun  7031  ccfunen  7047  elni2  7090  mulclpi  7104  nlt1pig  7117  indpi  7118  recclnq  7168  ltexnqq  7184  halfnqq  7186  prarloclemarch  7194  prarloclemarch2  7195  prop  7251  prltlu  7263  prarloclem3step  7272  prarloclem5  7276  prarloclem  7277  prarloc  7279  prarloc2  7280  genpml  7293  genpmu  7294  genprndl  7297  genprndu  7298  genpdisj  7299  addnqprllem  7303  addnqprulem  7304  addlocprlemeq  7309  addlocprlemgt  7310  addlocprlem  7311  addlocpr  7312  nqprloc  7321  nqprl  7327  nqpru  7328  addnqprlemrl  7333  addnqprlemru  7334  appdivnq  7339  prmuloc  7342  prmuloc2  7343  mullocprlem  7346  mullocpr  7347  mulnqprlemrl  7349  mulnqprlemru  7350  ltprordil  7365  ltpopr  7371  ltsopr  7372  ltaddpr  7373  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemlol  7378  ltexprlemopu  7379  ltexprlemupu  7380  ltexprlemloc  7383  ltexprlemfl  7385  ltexprlemrl  7386  ltexprlemfu  7387  ltexprlemru  7388  ltaprg  7395  recexprlemm  7400  recexprlem1ssl  7409  recexprlem1ssu  7410  aptiprleml  7415  aptiprlemu  7416  archpr  7419  cauappcvgprlemm  7421  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemopu  7424  cauappcvgprlemupu  7425  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  cauappcvgprlemladdru  7432  cauappcvgprlem1  7435  archrecpr  7440  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemopu  7447  caucvgprlemupu  7448  caucvgprlemdisj  7450  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprlem1  7455  caucvgprlemlim  7457  caucvgprprlemnbj  7469  caucvgprprlemml  7470  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemupu  7476  caucvgprprlemdisj  7478  caucvgprprlemloc  7479  caucvgprprlemexbt  7482  caucvgprprlemaddq  7484  caucvgprprlemlim  7487  suplocexprlemss  7491  suplocexprlemrl  7493  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  suplocexprlemlub  7500  recexgt0sr  7549  mulgt0sr  7554  archsr  7558  caucvgsrlemoffcau  7574  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  cnm  7608  axarch  7667  axcaucvglemcau  7674  axpre-suploclemres  7677  lelttr  7820  ltletr  7821  ltled  7849  cnegexlem1  7905  cnegexlem2  7906  renegcl  7991  negf1o  8112  gt0add  8302  apreap  8316  apirr  8334  apsym  8335  apcotr  8336  apadd1  8337  apneg  8340  mulext1  8341  mulap0r  8344  apti  8351  aprcl  8375  recexap  8381  mulap0  8382  receuap  8397  mul0eqap  8398  lep1  8567  lem1  8569  letrp1  8570  recreclt  8622  lbinf  8670  suprubex  8673  nnrecgt0  8722  bndndx  8934  nn0ge2m1nn  8995  elnn0z  9025  peano2z  9048  zaddcl  9052  ztri3or0  9054  zltnle  9058  zdceq  9084  zdcle  9085  zdclt  9086  zdiv  9097  zeo  9114  fnn0ind  9125  btwnz  9128  uzm1  9312  uzp1  9315  indstr  9344  supinfneg  9346  infsupneg  9347  eluzdc  9360  nn01to3  9365  qapne  9387  xrltled  9540  xrlelttr  9544  xrltletr  9545  ge0nemnf  9562  fzdcel  9775  elfzouz2  9893  fzoss1  9903  fzospliti  9908  fzocatel  9931  fzostep1  9969  qtri3or  9975  qltnle  9978  qdceq  9979  exbtwnzlemex  9982  rebtwn2zlemstep  9985  rebtwn2z  9987  qbtwnxr  9990  ioom  9993  ico0  9994  ioc0  9995  flqeqceilz  10046  modqadd1  10089  modqmul1  10105  frec2uzuzd  10130  frec2uzlt2d  10132  frec2uzf1od  10134  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgdomlem  10145  uzsinds  10170  seqvalcd  10187  seqovcd  10191  seq3fveq2  10197  seq3shft2  10201  monoord  10204  seq3split  10207  seq3caopr3  10209  iseqf1olemab  10217  iseqf1olemnanb  10218  iseqf1olemqk  10222  seq3id3  10235  seq3id2  10237  seq3homo  10238  expgt1  10286  m1expeven  10295  expnbnd  10370  expnlbnd2  10372  hashennn  10481  zfz1isolem1  10538  seq3coll  10540  cjap  10633  caucvgre  10708  cvg1nlemres  10712  resqrexlemgt0  10747  resqrexlemglsq  10749  resqrexlemga  10750  resqrtcl  10756  abslt  10815  abssubap0  10817  abssubne0  10818  caubnd2  10844  qdenre  10929  maxabslemlub  10934  maxabs  10936  maxleast  10940  fimaxre2  10953  xrmaxiflemlub  10972  xrmaxif  10975  xrmaxltsup  10982  xrmaxadd  10985  xrmineqinf  10993  climuni  11017  2clim  11025  climcn1  11032  climcn2  11033  subcn2  11035  mulcn2  11036  climsqz  11059  climsqz2  11060  climcau  11071  climcvg1nlem  11073  climcaucn  11075  serf0  11076  sumrbdclem  11100  summodclem2  11106  zsumdc  11108  divcnv  11221  absltap  11233  absgtap  11234  mertenslem2  11260  efcllemp  11278  tanvalap  11329  sin01bnd  11378  cos01bnd  11379  sin01gt0  11382  absef  11390  eirrap  11396  dvds0  11420  dvdsmul1  11427  dvdsmultr1d  11444  dvdslelemd  11453  divconjdvds  11459  alzdvds  11464  sqoddm1div8z  11495  nno  11515  divalglemex  11531  zsupcllemstep  11550  zsupcl  11552  infssuzledc  11555  dvdsbnd  11557  dvdslegcd  11565  zeqzmulgcd  11571  gcd0id  11579  gcdaddm  11584  gcd1  11587  gcdabs  11588  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlemex  11601  bezoutlemzz  11602  bezoutlemaz  11603  bezoutlembz  11604  bezoutlembi  11605  bezoutlemle  11608  bezoutlemsup  11609  mulgcd  11616  gcdzeq  11622  dvdsmulgcd  11625  sqgcd  11629  bezoutr1  11633  algcvga  11644  algfx  11645  eucalglt  11650  eucalg  11652  lcmneg  11667  lcmabs  11669  lcmgcdlem  11670  ncoprmgcdne1b  11682  mulgcddvds  11687  qredeq  11689  divgcdcoprm0  11694  cncongr1  11696  isprm2lem  11709  nprm  11716  dvdsnprmd  11718  prmdvdsfz  11731  coprm  11734  isprm6  11737  sqrt2irr  11752  pw2dvdslemn  11754  pw2dvdseulemle  11756  oddpwdclemdvds  11759  oddpwdclemndvds  11760  sqrt2irrap  11769  qnumdencl  11776  ennnfonelemex  11838  ennnfonelemhom  11839  ennnfonelemrnh  11840  ennnfonelemnn0  11846  ennnfonelemim  11848  exmidunben  11850  ctinfomlemom  11851  ctinfom  11852  ctinf  11854  tgcl  12144  neii1  12227  neii2  12229  neiss  12230  tpnei  12240  tgrest  12249  ssrest  12262  icnpimaex  12291  lmcvg  12297  cnpnei  12299  cnptopco  12302  lmff  12329  txcnp  12351  txcn  12355  hmeontr  12393  blssec  12518  mopni3  12564  blsscls2  12573  comet  12579  bdxmet  12581  bdmopn  12584  xmettxlem  12589  xmettx  12590  addcncntoplem  12631  mulc1cncf  12656  cncfco  12658  cncfmptc  12662  mulcncflem  12670  mulcncf  12671  dedekindeulemlu  12679  dedekindeulemeu  12680  suplociccreex  12682  suplociccex  12683  dedekindicclemlu  12688  dedekindicclemeu  12689  ivthinclemlopn  12694  ivthinclemlr  12695  ivthinclemuopn  12696  ivthinclemur  12697  ivthinclemloc  12699  ivthinc  12701  limcimolemlt  12713  limcresi  12715  cnplimcim  12716  cnplimclemle  12717  cnplimclemr  12718  limccnpcntop  12724  limccoap  12727  dvcoapbr  12751  dvcj  12753  sin0pilem2  12774  bj-exlimmpi  12873  uzdcinzz  12901  bj-2inf  13032  bj-peano4  13049  bj-nn0suc  13058  exmid1stab  13091  subctctexmid  13092  nninfalllem1  13099  nninfsellemqall  13107  nninfomnilem  13110  nninffeq  13112  exmidsbthrlem  13113  sbthomlem  13116  refeq  13119  isomninnlem  13121
  Copyright terms: Public domain W3C validator