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  36  mpdd  40  mp2d  46  pm2.43i  48  syl3c  62  mpbid  145  mpbird  165  jcai  304  mp2and  424  pm2.21dd  583  mt2d  588  mpjaod  671  impidc  791  jadc  796  pm2.54dc  826  stabtestimpdc  860  pm4.55dc  882  oplem1  919  mp3and  1274  xor3dc  1321  exlimdd  1797  exlimddv  1823  eqrdav  2084  necon1aidc  2302  necon1bidc  2303  necon4aidc  2319  reximddv  2472  rexlimddv  2489  vtoclgft  2663  rspcedvd  2721  sseldd  3015  ssneldd  3017  tpid3g  3538  preq12b  3597  axpweq  3981  opth  4038  issod  4120  frirrg  4151  frind  4153  ralxfr2d  4260  rexxfr2d  4261  eldifpw  4272  onun2  4280  onuni  4284  elirr  4330  en2lp  4343  wetriext  4365  peano2  4383  relop  4554  elres  4715  sotri2  4796  iota4an  4965  iota5  4966  funeu  5005  funopg  5013  imadiflem  5058  funimaexglem  5062  ssimaex  5328  ffvelrn  5395  dff3im  5407  dffo4  5410  f1eqcocnv  5531  f1oiso2  5567  riota5f  5593  riotass2  5595  acexmidlemcase  5608  ovmpt2df  5733  ovmpt2dv2  5735  ovi3  5738  ov6g  5739  caoftrn  5837  op1steq  5906  tfr0dm  6041  tfrlemibxssdm  6046  tfrlemi14d  6052  tfr1onlembxssdm  6062  tfr1onlemaccex  6067  tfr1onlemres  6068  tfrcllembxssdm  6075  tfrcllemaccex  6080  tfrcllemres  6081  rdgivallem  6100  nnsucelsuc  6206  nnsucsssuc  6207  dcdifsnid  6217  nnawordex  6239  ersym  6256  mapvalg  6367  pmvalg  6368  mapsn  6399  fundmen  6475  mapdom1g  6515  fidceq  6537  fin0or  6554  findcard2  6557  findcard2s  6558  suplub2ti  6640  supsnti  6644  supisoex  6648  enomnilem  6738  exmidomniim  6741  exmidomni  6742  fodjuomnilemdc  6743  fodjuomnilemres  6747  en2eleq  6765  elni2  6817  mulclpi  6831  nlt1pig  6844  indpi  6845  recclnq  6895  ltexnqq  6911  halfnqq  6913  prarloclemarch  6921  prarloclemarch2  6922  prop  6978  prltlu  6990  prarloclem3step  6999  prarloclem5  7003  prarloclem  7004  prarloc  7006  prarloc2  7007  genpml  7020  genpmu  7021  genprndl  7024  genprndu  7025  genpdisj  7026  addnqprllem  7030  addnqprulem  7031  addlocprlemeq  7036  addlocprlemgt  7037  addlocprlem  7038  addlocpr  7039  nqprloc  7048  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  appdivnq  7066  prmuloc  7069  prmuloc2  7070  mullocprlem  7073  mullocpr  7074  mulnqprlemrl  7076  mulnqprlemru  7077  ltprordil  7092  ltpopr  7098  ltsopr  7099  ltaddpr  7100  ltexprlemm  7103  ltexprlemopl  7104  ltexprlemlol  7105  ltexprlemopu  7106  ltexprlemupu  7107  ltexprlemloc  7110  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  ltaprg  7122  recexprlemm  7127  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprleml  7142  aptiprlemu  7143  archpr  7146  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemupu  7152  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlem1  7162  archrecpr  7167  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemupu  7175  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlem1  7182  caucvgprlemlim  7184  caucvgprprlemnbj  7196  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemupu  7203  caucvgprprlemdisj  7205  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlemaddq  7211  caucvgprprlemlim  7214  recexgt0sr  7263  mulgt0sr  7267  archsr  7271  caucvgsrlemoffcau  7287  axarch  7370  axcaucvglemcau  7377  lelttr  7517  ltletr  7518  ltled  7546  cnegexlem1  7601  cnegexlem2  7602  renegcl  7687  negf1o  7804  gt0add  7991  apreap  8005  apirr  8023  apsym  8024  apcotr  8025  apadd1  8026  apneg  8029  mulext1  8030  mulap0r  8033  apti  8040  recexap  8061  mulap0  8062  receuap  8077  lep1  8241  lem1  8243  letrp1  8244  recreclt  8296  lbinf  8344  suprubex  8347  nnrecgt0  8394  bndndx  8605  nn0ge2m1nn  8666  elnn0z  8696  peano2z  8719  zaddcl  8723  ztri3or0  8725  zltnle  8729  zdceq  8755  zdcle  8756  zdclt  8757  zdiv  8767  zeo  8784  fnn0ind  8795  btwnz  8798  uzm1  8981  uzp1  8984  indstr  9013  supinfneg  9015  infsupneg  9016  eluzdc  9029  nn01to3  9034  qapne  9056  xrlelttr  9203  xrltletr  9204  ge0nemnf  9218  fzdcel  9386  elfzouz2  9500  fzoss1  9510  fzospliti  9515  fzocatel  9538  fzostep1  9576  qtri3or  9582  qltnle  9585  qdceq  9586  exbtwnzlemex  9589  rebtwn2zlemstep  9592  rebtwn2z  9594  qbtwnxr  9597  ioom  9600  ico0  9601  ioc0  9602  flqeqceilz  9653  modqadd1  9696  modqmul1  9712  frec2uzuzd  9737  frec2uzlt2d  9739  frec2uzf1od  9741  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgdomlem  9752  uzsinds  9776  iseqval  9788  iseqss  9800  iseqfveq2  9803  iseqshft2  9807  monoord  9810  iseqsplit  9813  iseqcaopr3  9815  iseqf1olemab  9823  iseqf1olemnanb  9824  iseqf1olemqk  9828  iseqid3s  9842  iseqid2  9844  iseqhomo  9845  expgt1  9892  m1expeven  9901  expnbnd  9974  expnlbnd2  9976  hashennn  10085  zfz1isolem1  10142  iseqcoll  10144  cjap  10236  caucvgre  10310  cvg1nlemres  10314  resqrexlemgt0  10349  resqrexlemglsq  10351  resqrexlemga  10352  resqrtcl  10358  abslt  10417  abssubap0  10419  abssubne0  10420  caubnd2  10446  qdenre  10531  maxabslemlub  10536  maxabs  10538  maxleast  10542  fimaxre2  10553  climuni  10576  2clim  10584  climcn1  10591  climcn2  10592  subcn2  10594  mulcn2  10595  climsqz  10617  climsqz2  10618  climcau  10628  climcvg1nlem  10630  climcaucn  10632  serif0  10633  isumrblem  10657  isummolem2  10663  zisum  10665  dvds0  10693  dvdsmul1  10700  dvdsmultr1d  10717  dvdslelemd  10726  divconjdvds  10732  alzdvds  10737  sqoddm1div8z  10768  nno  10788  divalglemex  10804  zsupcllemstep  10823  zsupcl  10825  infssuzledc  10828  dvdsbnd  10830  dvdslegcd  10838  zeqzmulgcd  10844  gcd0id  10852  gcdaddm  10857  gcd1  10860  gcdabs  10861  bezoutlemnewy  10867  bezoutlemstep  10868  bezoutlemmain  10869  bezoutlemex  10872  bezoutlemzz  10873  bezoutlemaz  10874  bezoutlembz  10875  bezoutlembi  10876  bezoutlemle  10879  bezoutlemsup  10880  mulgcd  10887  gcdzeq  10893  dvdsmulgcd  10896  sqgcd  10900  bezoutr1  10904  ialgcvga  10915  ialgfx  10916  eucalglt  10921  eucialg  10923  lcmneg  10938  lcmabs  10940  lcmgcdlem  10941  ncoprmgcdne1b  10953  mulgcddvds  10958  qredeq  10960  divgcdcoprm0  10965  cncongr1  10967  isprm2lem  10980  nprm  10987  dvdsnprmd  10989  prmdvdsfz  11002  coprm  11005  isprm6  11008  sqrt2irr  11023  pw2dvdslemn  11025  pw2dvdseulemle  11027  oddpwdclemdvds  11030  oddpwdclemndvds  11031  sqrt2irrap  11040  qnumdencl  11047  bj-exlimmpi  11116  uzdcinzz  11143  bj-2inf  11278  bj-peano4  11295  bj-nn0suc  11304  nninfalllem1  11344  nninfsellemqall  11352  nninfomnilem  11355  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator