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  789  jadc  794  pm2.54dc  824  stabtestimpdc  858  pm4.55dc  880  oplem1  917  mp3and  1272  xor3dc  1319  exlimdd  1794  exlimddv  1820  eqrdav  2081  necon1aidc  2297  necon1bidc  2298  necon4aidc  2314  reximddv  2465  rexlimddv  2482  vtoclgft  2650  rspcdva  2708  rspcedvd  2709  sseldd  3001  ssneldd  3003  tpid3g  3513  preq12b  3570  axpweq  3953  opth  4000  issod  4082  frirrg  4113  frind  4115  ralxfr2d  4222  rexxfr2d  4223  eldifpw  4234  onun2  4242  onuni  4246  elirr  4292  en2lp  4305  wetriext  4327  peano2  4344  relop  4514  elres  4674  sotri2  4752  iota4an  4916  iota5  4917  funeu  4956  funopg  4964  imadiflem  5009  funimaexglem  5013  ssimaex  5266  ffvelrn  5332  dff3im  5344  dffo4  5347  f1eqcocnv  5462  f1oiso2  5497  riota5f  5523  riotass2  5525  acexmidlemcase  5538  ovmpt2df  5663  ovmpt2dv2  5665  ovi3  5668  ov6g  5669  caoftrn  5767  op1steq  5836  tfr0dm  5971  tfrlemibxssdm  5976  tfrlemi14d  5982  tfr1onlembxssdm  5992  tfr1onlemaccex  5997  tfr1onlemres  5998  tfrcllembxssdm  6005  tfrcllemaccex  6010  tfrcllemres  6011  rdgivallem  6030  nnsucelsuc  6135  nnsucsssuc  6136  nnawordex  6167  ersym  6184  fundmen  6353  fidceq  6404  fin0or  6420  findcard2  6423  findcard2s  6424  suplub2ti  6473  supsnti  6477  supisoex  6481  en2eleq  6521  elni2  6566  mulclpi  6580  nlt1pig  6593  indpi  6594  recclnq  6644  ltexnqq  6660  halfnqq  6662  prarloclemarch  6670  prarloclemarch2  6671  prop  6727  prltlu  6739  prarloclem3step  6748  prarloclem5  6752  prarloclem  6753  prarloc  6755  prarloc2  6756  genpml  6769  genpmu  6770  genprndl  6773  genprndu  6774  genpdisj  6775  addnqprllem  6779  addnqprulem  6780  addlocprlemeq  6785  addlocprlemgt  6786  addlocprlem  6787  addlocpr  6788  nqprloc  6797  nqprl  6803  nqpru  6804  addnqprlemrl  6809  addnqprlemru  6810  appdivnq  6815  prmuloc  6818  prmuloc2  6819  mullocprlem  6822  mullocpr  6823  mulnqprlemrl  6825  mulnqprlemru  6826  ltprordil  6841  ltpopr  6847  ltsopr  6848  ltaddpr  6849  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  ltexprlemloc  6859  ltexprlemfl  6861  ltexprlemrl  6862  ltexprlemfu  6863  ltexprlemru  6864  ltaprg  6871  recexprlemm  6876  recexprlem1ssl  6885  recexprlem1ssu  6886  aptiprleml  6891  aptiprlemu  6892  archpr  6895  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemupu  6901  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlem1  6911  archrecpr  6916  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemupu  6924  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlem1  6931  caucvgprlemlim  6933  caucvgprprlemnbj  6945  caucvgprprlemml  6946  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemupu  6952  caucvgprprlemdisj  6954  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlemaddq  6960  caucvgprprlemlim  6963  recexgt0sr  7012  mulgt0sr  7016  archsr  7020  caucvgsrlemoffcau  7036  axarch  7119  axcaucvglemcau  7126  lelttr  7266  ltletr  7267  ltled  7295  cnegexlem1  7350  cnegexlem2  7351  renegcl  7436  negf1o  7553  gt0add  7740  apreap  7754  apirr  7772  apsym  7773  apcotr  7774  apadd1  7775  apneg  7778  mulext1  7779  mulap0r  7782  apti  7789  recexap  7810  mulap0  7811  receuap  7826  lep1  7990  lem1  7992  letrp1  7993  recreclt  8045  lbinf  8093  suprubex  8096  nnrecgt0  8143  bndndx  8354  nn0ge2m1nn  8415  elnn0z  8445  peano2z  8468  zaddcl  8472  ztri3or0  8474  zltnle  8478  zdceq  8504  zdcle  8505  zdclt  8506  zdiv  8516  zeo  8533  fnn0ind  8544  btwnz  8547  uzm1  8730  uzp1  8733  indstr  8762  supinfneg  8764  infsupneg  8765  eluzdc  8778  nn01to3  8783  qapne  8805  xrlelttr  8952  xrltletr  8953  ge0nemnf  8967  fzdcel  9135  elfzouz2  9247  fzoss1  9257  fzospliti  9262  fzocatel  9285  fzostep1  9323  qtri3or  9329  qltnle  9332  qdceq  9333  exbtwnzlemex  9336  rebtwn2zlemstep  9339  rebtwn2z  9341  qbtwnxr  9344  ioom  9347  ico0  9348  ioc0  9349  flqeqceilz  9400  modqadd1  9443  modqmul1  9459  frec2uzuzd  9484  frec2uzlt2d  9486  frec2uzf1od  9488  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgdomlem  9499  uzsinds  9518  iseqval  9530  iseqss  9541  iseqfveq2  9544  iseqshft2  9548  monoord  9551  iseqsplit  9554  iseqcaopr3  9556  iseqid3s  9562  iseqid2  9564  iseqhomo  9565  expgt1  9611  m1expeven  9620  expnbnd  9693  expnlbnd2  9695  sizeennn  9804  cjap  9931  caucvgre  10005  cvg1nlemres  10009  resqrexlemgt0  10044  resqrexlemglsq  10046  resqrexlemga  10047  resqrtcl  10053  abslt  10112  abssubap0  10114  abssubne0  10115  caubnd2  10141  qdenre  10226  maxabslemlub  10231  maxabs  10233  maxleast  10237  fimaxre2  10247  climuni  10270  2clim  10278  climcn1  10285  climcn2  10286  subcn2  10288  mulcn2  10289  climsqz  10311  climsqz2  10312  climcau  10322  climcvg1nlem  10324  climcaucn  10326  serif0  10327  isumrblem  10337  dvds0  10355  dvdsmul1  10362  dvdsmultr1d  10379  dvdslelemd  10388  divconjdvds  10394  alzdvds  10399  sqoddm1div8z  10430  nno  10450  divalglemex  10466  zsupcllemstep  10485  zsupcl  10487  infssuzledc  10490  dvdsbnd  10492  dvdslegcd  10500  zeqzmulgcd  10506  gcd0id  10514  gcdaddm  10519  gcd1  10522  gcdabs  10523  bezoutlemnewy  10529  bezoutlemstep  10530  bezoutlemmain  10531  bezoutlemex  10534  bezoutlemzz  10535  bezoutlemaz  10536  bezoutlembz  10537  bezoutlembi  10538  bezoutlemle  10541  bezoutlemsup  10542  mulgcd  10549  gcdzeq  10555  dvdsmulgcd  10558  sqgcd  10562  bezoutr1  10566  ialgcvga  10577  ialgfx  10578  eucalglt  10583  eucialg  10585  lcmneg  10600  lcmabs  10602  lcmgcdlem  10603  ncoprmgcdne1b  10615  mulgcddvds  10620  qredeq  10622  divgcdcoprm0  10627  cncongr1  10629  isprm2lem  10642  nprm  10649  dvdsnprmd  10651  prmdvdsfz  10664  coprm  10667  isprm6  10670  sqrt2irr  10685  pw2dvdslemn  10687  pw2dvdseulemle  10689  oddpwdclemdvds  10692  oddpwdclemndvds  10693  sqrt2irrap  10702  bj-exlimmpi  10732  uzdcinzz  10759  bj-2inf  10891  bj-peano4  10908  bj-nn0suc  10917
  Copyright terms: Public domain W3C validator