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 5 1 (𝜑𝜒)
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  609  mt2d  614  mpjaod  707  stdcndcOLD  831  impidc  843  jadc  848  pm2.54dc  876  pm4.55dc  922  oplem1  959  mp3and  1318  xor3dc  1365  exlimdd  1844  exlimddv  1870  eqrdav  2138  necon1aidc  2359  necon1bidc  2360  necon4aidc  2376  reximddv  2535  reximssdv  2536  rexlimddv  2554  vtoclgft  2736  rspcedvd  2795  sseldd  3098  ssneldd  3100  tpid3g  3638  preq12b  3697  axpweq  4095  exmid1dc  4123  opth  4159  issod  4241  frirrg  4272  frind  4274  ralxfr2d  4385  rexxfr2d  4386  eldifpw  4398  onun2  4406  onuni  4410  elirr  4456  en2lp  4469  wetriext  4491  peano2  4509  relop  4689  elres  4855  sotri2  4936  iota4an  5107  iota5  5108  funeu  5148  funopg  5157  imadiflem  5202  funimaexglem  5206  ssimaex  5482  ffvelrn  5553  dff3im  5565  dffo4  5568  f1eqcocnv  5692  f1oiso2  5728  riota5f  5754  riotass2  5756  acexmidlemcase  5769  ovmpodf  5902  ovmpodv2  5904  ovi3  5907  ov6g  5908  caoftrn  6007  op1steq  6077  tfr0dm  6219  tfrlemibxssdm  6224  tfrlemi14d  6230  tfr1onlembxssdm  6240  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllembxssdm  6253  tfrcllemaccex  6258  tfrcllemres  6259  rdgivallem  6278  nnsucelsuc  6387  nnsucsssuc  6388  dcdifsnid  6400  nnawordex  6424  ersym  6441  mapvalg  6552  pmvalg  6553  mapsn  6584  fundmen  6700  mapdom1g  6741  fidceq  6763  fin0or  6780  findcard2  6783  findcard2s  6784  fiintim  6817  suplub2ti  6888  supsnti  6892  supisoex  6896  difinfsnlem  6984  difinfsn  6985  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  enomnilem  7010  exmidomniim  7013  exmidomni  7014  fodjuomnilemdc  7016  fodjuomnilemres  7020  omnimkv  7030  mkvprop  7032  en2eleq  7051  acfun  7063  ccfunen  7079  cc4f  7084  cc4n  7086  elni2  7129  mulclpi  7143  nlt1pig  7156  indpi  7157  recclnq  7207  ltexnqq  7223  halfnqq  7225  prarloclemarch  7233  prarloclemarch2  7234  prop  7290  prltlu  7302  prarloclem3step  7311  prarloclem5  7315  prarloclem  7316  prarloc  7318  prarloc2  7319  genpml  7332  genpmu  7333  genprndl  7336  genprndu  7337  genpdisj  7338  addnqprllem  7342  addnqprulem  7343  addlocprlemeq  7348  addlocprlemgt  7349  addlocprlem  7350  addlocpr  7351  nqprloc  7360  nqprl  7366  nqpru  7367  addnqprlemrl  7372  addnqprlemru  7373  appdivnq  7378  prmuloc  7381  prmuloc2  7382  mullocprlem  7385  mullocpr  7386  mulnqprlemrl  7388  mulnqprlemru  7389  ltprordil  7404  ltpopr  7410  ltsopr  7411  ltaddpr  7412  ltexprlemm  7415  ltexprlemopl  7416  ltexprlemlol  7417  ltexprlemopu  7418  ltexprlemupu  7419  ltexprlemloc  7422  ltexprlemfl  7424  ltexprlemrl  7425  ltexprlemfu  7426  ltexprlemru  7427  ltaprg  7434  recexprlemm  7439  recexprlem1ssl  7448  recexprlem1ssu  7449  aptiprleml  7454  aptiprlemu  7455  archpr  7458  cauappcvgprlemm  7460  cauappcvgprlemopl  7461  cauappcvgprlemlol  7462  cauappcvgprlemopu  7463  cauappcvgprlemupu  7464  cauappcvgprlemdisj  7466  cauappcvgprlemloc  7467  cauappcvgprlemladdfu  7469  cauappcvgprlemladdfl  7470  cauappcvgprlemladdru  7471  cauappcvgprlem1  7474  archrecpr  7479  caucvgprlemnkj  7481  caucvgprlemnbj  7482  caucvgprlemm  7483  caucvgprlemopl  7484  caucvgprlemlol  7485  caucvgprlemopu  7486  caucvgprlemupu  7487  caucvgprlemdisj  7489  caucvgprlemloc  7490  caucvgprlemladdfu  7492  caucvgprlem1  7494  caucvgprlemlim  7496  caucvgprprlemnbj  7508  caucvgprprlemml  7509  caucvgprprlemopl  7512  caucvgprprlemlol  7513  caucvgprprlemopu  7514  caucvgprprlemupu  7515  caucvgprprlemdisj  7517  caucvgprprlemloc  7518  caucvgprprlemexbt  7521  caucvgprprlemaddq  7523  caucvgprprlemlim  7526  suplocexprlemss  7530  suplocexprlemrl  7532  suplocexprlemmu  7533  suplocexprlemru  7534  suplocexprlemdisj  7535  suplocexprlemloc  7536  suplocexprlemub  7538  suplocexprlemlub  7539  recexgt0sr  7588  mulgt0sr  7593  archsr  7597  caucvgsrlemoffcau  7613  suplocsrlemb  7621  suplocsrlempr  7622  suplocsrlem  7623  cnm  7647  axarch  7706  axcaucvglemcau  7713  axpre-suploclemres  7716  lelttr  7859  ltletr  7860  ltled  7888  cnegexlem1  7944  cnegexlem2  7945  renegcl  8030  negf1o  8151  gt0add  8342  apreap  8356  apirr  8374  apsym  8375  apcotr  8376  apadd1  8377  apneg  8380  mulext1  8381  mulap0r  8384  apti  8391  aprcl  8415  recexap  8421  mulap0  8422  receuap  8437  mul0eqap  8438  lep1  8610  lem1  8612  letrp1  8613  recreclt  8665  lbinf  8713  suprubex  8716  nnrecgt0  8765  bndndx  8983  nn0ge2m1nn  9044  elnn0z  9074  peano2z  9097  zaddcl  9101  ztri3or0  9103  zltnle  9107  zdceq  9133  zdcle  9134  zdclt  9135  zdiv  9146  zeo  9163  fnn0ind  9174  btwnz  9177  uzm1  9363  uzp1  9366  indstr  9395  supinfneg  9397  infsupneg  9398  eluzdc  9411  nn01to3  9416  qapne  9438  xrltled  9592  xrlelttr  9596  xrltletr  9597  ge0nemnf  9614  fzdcel  9827  elfzouz2  9945  fzoss1  9955  fzospliti  9960  fzocatel  9983  fzostep1  10021  qtri3or  10027  qltnle  10030  qdceq  10031  exbtwnzlemex  10034  rebtwn2zlemstep  10037  rebtwn2z  10039  qbtwnxr  10042  ioom  10045  ico0  10046  ioc0  10047  flqeqceilz  10098  modqadd1  10141  modqmul1  10157  frec2uzuzd  10182  frec2uzlt2d  10184  frec2uzf1od  10186  frecuzrdgrrn  10188  frec2uzrdg  10189  frecuzrdgrcl  10190  frecuzrdgsuc  10194  frecuzrdgrclt  10195  frecuzrdgdomlem  10197  uzsinds  10222  seqvalcd  10239  seqovcd  10243  seq3fveq2  10249  seq3shft2  10253  monoord  10256  seq3split  10259  seq3caopr3  10261  iseqf1olemab  10269  iseqf1olemnanb  10270  iseqf1olemqk  10274  seq3id3  10287  seq3id2  10289  seq3homo  10290  expgt1  10338  m1expeven  10347  expnbnd  10422  expnlbnd2  10424  hashennn  10533  zfz1isolem1  10590  seq3coll  10592  cjap  10685  caucvgre  10760  cvg1nlemres  10764  resqrexlemgt0  10799  resqrexlemglsq  10801  resqrexlemga  10802  resqrtcl  10808  abslt  10867  abssubap0  10869  abssubne0  10870  caubnd2  10896  qdenre  10981  maxabslemlub  10986  maxabs  10988  maxleast  10992  fimaxre2  11005  xrmaxiflemlub  11024  xrmaxif  11027  xrmaxltsup  11034  xrmaxadd  11037  xrmineqinf  11045  climuni  11069  2clim  11077  climcn1  11084  climcn2  11085  subcn2  11087  mulcn2  11088  climsqz  11111  climsqz2  11112  climcau  11123  climcvg1nlem  11125  climcaucn  11127  serf0  11128  sumrbdclem  11153  summodclem2  11158  zsumdc  11160  divcnv  11273  absltap  11285  absgtap  11286  mertenslem2  11312  ntrivcvgap  11324  prodrbdclem  11347  prodmodclem2  11353  efcllemp  11371  tanvalap  11422  sin01bnd  11471  cos01bnd  11472  sin01gt0  11475  absef  11483  eirrap  11491  dvds0  11515  dvdsmul1  11522  dvdsmultr1d  11539  dvdslelemd  11548  divconjdvds  11554  alzdvds  11559  sqoddm1div8z  11590  nno  11610  divalglemex  11626  zsupcllemstep  11645  zsupcl  11647  infssuzledc  11650  dvdsbnd  11652  dvdslegcd  11660  zeqzmulgcd  11666  gcd0id  11674  gcdaddm  11679  gcd1  11682  gcdabs  11683  bezoutlemnewy  11691  bezoutlemstep  11692  bezoutlemmain  11693  bezoutlemex  11696  bezoutlemzz  11697  bezoutlemaz  11698  bezoutlembz  11699  bezoutlembi  11700  bezoutlemle  11703  bezoutlemsup  11704  mulgcd  11711  gcdzeq  11717  dvdsmulgcd  11720  sqgcd  11724  bezoutr1  11728  algcvga  11739  algfx  11740  eucalglt  11745  eucalg  11747  lcmneg  11762  lcmabs  11764  lcmgcdlem  11765  ncoprmgcdne1b  11777  mulgcddvds  11782  qredeq  11784  divgcdcoprm0  11789  cncongr1  11791  isprm2lem  11804  nprm  11811  dvdsnprmd  11813  prmdvdsfz  11826  coprm  11829  isprm6  11832  sqrt2irr  11847  pw2dvdslemn  11850  pw2dvdseulemle  11852  oddpwdclemdvds  11855  oddpwdclemndvds  11856  sqrt2irrap  11865  qnumdencl  11872  ennnfonelemex  11934  ennnfonelemhom  11935  ennnfonelemrnh  11936  ennnfonelemnn0  11942  ennnfonelemim  11944  exmidunben  11946  ctinfomlemom  11947  ctinfom  11948  ctinf  11950  omctfn  11963  tgcl  12243  neii1  12326  neii2  12328  neiss  12329  tpnei  12339  tgrest  12348  ssrest  12361  icnpimaex  12390  lmcvg  12396  cnpnei  12398  cnptopco  12401  lmff  12428  txcnp  12450  txcn  12454  hmeontr  12492  blssec  12617  mopni3  12663  blsscls2  12672  comet  12678  bdxmet  12680  bdmopn  12683  xmettxlem  12688  xmettx  12689  addcncntoplem  12730  mulc1cncf  12755  cncfco  12757  cncfmptc  12761  mulcncflem  12769  mulcncf  12770  dedekindeulemlu  12778  dedekindeulemeu  12779  suplociccreex  12781  suplociccex  12782  dedekindicclemlu  12787  dedekindicclemeu  12788  ivthinclemlopn  12793  ivthinclemlr  12794  ivthinclemuopn  12795  ivthinclemur  12796  ivthinclemloc  12798  ivthinc  12800  limcimolemlt  12812  limcresi  12814  cnplimcim  12815  cnplimclemle  12816  cnplimclemr  12817  limccnpcntop  12823  limccoap  12826  dvcoapbr  12850  dvcj  12852  sin0pilem2  12876  tangtx  12932  bj-exlimmpi  13007  uzdcinzz  13035  bj-2inf  13166  bj-peano4  13183  bj-nn0suc  13192  exmid1stab  13225  subctctexmid  13226  nninfalllem1  13233  nninfsellemqall  13241  nninfomnilem  13244  nninffeq  13246  exmidsbthrlem  13247  sbthomlem  13250  refeq  13253  isomninnlem  13255  apdifflemr  13268
  Copyright terms: Public domain W3C validator