ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpd GIF version

Theorem mpd 13
Description: A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpd.1 (𝜑𝜓)
mpd.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpd (𝜑𝜒)

Proof of Theorem mpd
StepHypRef Expression
1 mpd.1 . 2 (𝜑𝜓)
2 mpd.2 . . 3 (𝜑 → (𝜓𝜒))
32a2i 11 . 2 ((𝜑𝜓) → (𝜑𝜒))
41, 3ax-mp 7 1 (𝜑𝜒)
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  1795  exlimddv  1821  eqrdav  2082  necon1aidc  2300  necon1bidc  2301  necon4aidc  2317  reximddv  2470  rexlimddv  2487  vtoclgft  2660  rspcedvd  2718  sseldd  3011  ssneldd  3013  tpid3g  3529  preq12b  3588  axpweq  3971  opth  4028  issod  4110  frirrg  4141  frind  4143  ralxfr2d  4250  rexxfr2d  4251  eldifpw  4262  onun2  4270  onuni  4274  elirr  4320  en2lp  4333  wetriext  4355  peano2  4373  relop  4544  elres  4705  sotri2  4784  iota4an  4953  iota5  4954  funeu  4993  funopg  5001  imadiflem  5046  funimaexglem  5050  ssimaex  5310  ffvelrn  5377  dff3im  5389  dffo4  5392  f1eqcocnv  5510  f1oiso2  5545  riota5f  5571  riotass2  5573  acexmidlemcase  5586  ovmpt2df  5711  ovmpt2dv2  5713  ovi3  5716  ov6g  5717  caoftrn  5815  op1steq  5884  tfr0dm  6019  tfrlemibxssdm  6024  tfrlemi14d  6030  tfr1onlembxssdm  6040  tfr1onlemaccex  6045  tfr1onlemres  6046  tfrcllembxssdm  6053  tfrcllemaccex  6058  tfrcllemres  6059  rdgivallem  6078  nnsucelsuc  6184  nnsucsssuc  6185  dcdifsnid  6195  nnawordex  6217  ersym  6234  mapvalg  6345  pmvalg  6346  mapsn  6377  fundmen  6453  mapdom1g  6493  fidceq  6515  fin0or  6532  findcard2  6535  findcard2s  6536  suplub2ti  6603  supsnti  6607  supisoex  6611  enomnilem  6699  exmidomniim  6702  exmidomni  6703  fodjuomnilemdc  6704  fodjuomnilemres  6708  en2eleq  6724  elni2  6776  mulclpi  6790  nlt1pig  6803  indpi  6804  recclnq  6854  ltexnqq  6870  halfnqq  6872  prarloclemarch  6880  prarloclemarch2  6881  prop  6937  prltlu  6949  prarloclem3step  6958  prarloclem5  6962  prarloclem  6963  prarloc  6965  prarloc2  6966  genpml  6979  genpmu  6980  genprndl  6983  genprndu  6984  genpdisj  6985  addnqprllem  6989  addnqprulem  6990  addlocprlemeq  6995  addlocprlemgt  6996  addlocprlem  6997  addlocpr  6998  nqprloc  7007  nqprl  7013  nqpru  7014  addnqprlemrl  7019  addnqprlemru  7020  appdivnq  7025  prmuloc  7028  prmuloc2  7029  mullocprlem  7032  mullocpr  7033  mulnqprlemrl  7035  mulnqprlemru  7036  ltprordil  7051  ltpopr  7057  ltsopr  7058  ltaddpr  7059  ltexprlemm  7062  ltexprlemopl  7063  ltexprlemlol  7064  ltexprlemopu  7065  ltexprlemupu  7066  ltexprlemloc  7069  ltexprlemfl  7071  ltexprlemrl  7072  ltexprlemfu  7073  ltexprlemru  7074  ltaprg  7081  recexprlemm  7086  recexprlem1ssl  7095  recexprlem1ssu  7096  aptiprleml  7101  aptiprlemu  7102  archpr  7105  cauappcvgprlemm  7107  cauappcvgprlemopl  7108  cauappcvgprlemlol  7109  cauappcvgprlemopu  7110  cauappcvgprlemupu  7111  cauappcvgprlemdisj  7113  cauappcvgprlemloc  7114  cauappcvgprlemladdfu  7116  cauappcvgprlemladdfl  7117  cauappcvgprlemladdru  7118  cauappcvgprlem1  7121  archrecpr  7126  caucvgprlemnkj  7128  caucvgprlemnbj  7129  caucvgprlemm  7130  caucvgprlemopl  7131  caucvgprlemlol  7132  caucvgprlemopu  7133  caucvgprlemupu  7134  caucvgprlemdisj  7136  caucvgprlemloc  7137  caucvgprlemladdfu  7139  caucvgprlem1  7141  caucvgprlemlim  7143  caucvgprprlemnbj  7155  caucvgprprlemml  7156  caucvgprprlemopl  7159  caucvgprprlemlol  7160  caucvgprprlemopu  7161  caucvgprprlemupu  7162  caucvgprprlemdisj  7164  caucvgprprlemloc  7165  caucvgprprlemexbt  7168  caucvgprprlemaddq  7170  caucvgprprlemlim  7173  recexgt0sr  7222  mulgt0sr  7226  archsr  7230  caucvgsrlemoffcau  7246  axarch  7329  axcaucvglemcau  7336  lelttr  7476  ltletr  7477  ltled  7505  cnegexlem1  7560  cnegexlem2  7561  renegcl  7646  negf1o  7763  gt0add  7950  apreap  7964  apirr  7982  apsym  7983  apcotr  7984  apadd1  7985  apneg  7988  mulext1  7989  mulap0r  7992  apti  7999  recexap  8020  mulap0  8021  receuap  8036  lep1  8200  lem1  8202  letrp1  8203  recreclt  8255  lbinf  8303  suprubex  8306  nnrecgt0  8353  bndndx  8564  nn0ge2m1nn  8625  elnn0z  8659  peano2z  8682  zaddcl  8686  ztri3or0  8688  zltnle  8692  zdceq  8718  zdcle  8719  zdclt  8720  zdiv  8730  zeo  8747  fnn0ind  8758  btwnz  8761  uzm1  8944  uzp1  8947  indstr  8976  supinfneg  8978  infsupneg  8979  eluzdc  8992  nn01to3  8997  qapne  9019  xrlelttr  9166  xrltletr  9167  ge0nemnf  9181  fzdcel  9349  elfzouz2  9461  fzoss1  9471  fzospliti  9476  fzocatel  9499  fzostep1  9537  qtri3or  9543  qltnle  9546  qdceq  9547  exbtwnzlemex  9550  rebtwn2zlemstep  9553  rebtwn2z  9555  qbtwnxr  9558  ioom  9561  ico0  9562  ioc0  9563  flqeqceilz  9614  modqadd1  9657  modqmul1  9673  frec2uzuzd  9698  frec2uzlt2d  9700  frec2uzf1od  9702  frecuzrdgrrn  9704  frec2uzrdg  9705  frecuzrdgrcl  9706  frecuzrdgsuc  9710  frecuzrdgrclt  9711  frecuzrdgdomlem  9713  uzsinds  9737  iseqval  9749  iseqss  9760  iseqfveq2  9763  iseqshft2  9767  monoord  9770  iseqsplit  9773  iseqcaopr3  9775  iseqid3s  9781  iseqid2  9783  iseqhomo  9784  expgt1  9830  m1expeven  9839  expnbnd  9912  expnlbnd2  9914  hashennn  10023  cjap  10167  caucvgre  10241  cvg1nlemres  10245  resqrexlemgt0  10280  resqrexlemglsq  10282  resqrexlemga  10283  resqrtcl  10289  abslt  10348  abssubap0  10350  abssubne0  10351  caubnd2  10377  qdenre  10462  maxabslemlub  10467  maxabs  10469  maxleast  10473  fimaxre2  10483  climuni  10506  2clim  10514  climcn1  10521  climcn2  10522  subcn2  10524  mulcn2  10525  climsqz  10547  climsqz2  10548  climcau  10558  climcvg1nlem  10560  climcaucn  10562  serif0  10563  isumrblem  10573  dvds0  10591  dvdsmul1  10598  dvdsmultr1d  10615  dvdslelemd  10624  divconjdvds  10630  alzdvds  10635  sqoddm1div8z  10666  nno  10686  divalglemex  10702  zsupcllemstep  10721  zsupcl  10723  infssuzledc  10726  dvdsbnd  10728  dvdslegcd  10736  zeqzmulgcd  10742  gcd0id  10750  gcdaddm  10755  gcd1  10758  gcdabs  10759  bezoutlemnewy  10765  bezoutlemstep  10766  bezoutlemmain  10767  bezoutlemex  10770  bezoutlemzz  10771  bezoutlemaz  10772  bezoutlembz  10773  bezoutlembi  10774  bezoutlemle  10777  bezoutlemsup  10778  mulgcd  10785  gcdzeq  10791  dvdsmulgcd  10794  sqgcd  10798  bezoutr1  10802  ialgcvga  10813  ialgfx  10814  eucalglt  10819  eucialg  10821  lcmneg  10836  lcmabs  10838  lcmgcdlem  10839  ncoprmgcdne1b  10851  mulgcddvds  10856  qredeq  10858  divgcdcoprm0  10863  cncongr1  10865  isprm2lem  10878  nprm  10885  dvdsnprmd  10887  prmdvdsfz  10900  coprm  10903  isprm6  10906  sqrt2irr  10921  pw2dvdslemn  10923  pw2dvdseulemle  10925  oddpwdclemdvds  10928  oddpwdclemndvds  10929  sqrt2irrap  10938  qnumdencl  10945  bj-exlimmpi  11014  uzdcinzz  11041  bj-2inf  11176  bj-peano4  11193  bj-nn0suc  11202
  Copyright terms: Public domain W3C validator