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  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  8303  apreap  8317  apirr  8335  apsym  8336  apcotr  8337  apadd1  8338  apneg  8341  mulext1  8342  mulap0r  8345  apti  8352  aprcl  8376  recexap  8382  mulap0  8383  receuap  8398  mul0eqap  8399  lep1  8571  lem1  8573  letrp1  8574  recreclt  8626  lbinf  8674  suprubex  8677  nnrecgt0  8726  bndndx  8944  nn0ge2m1nn  9005  elnn0z  9035  peano2z  9058  zaddcl  9062  ztri3or0  9064  zltnle  9068  zdceq  9094  zdcle  9095  zdclt  9096  zdiv  9107  zeo  9124  fnn0ind  9135  btwnz  9138  uzm1  9324  uzp1  9327  indstr  9356  supinfneg  9358  infsupneg  9359  eluzdc  9372  nn01to3  9377  qapne  9399  xrltled  9553  xrlelttr  9557  xrltletr  9558  ge0nemnf  9575  fzdcel  9788  elfzouz2  9906  fzoss1  9916  fzospliti  9921  fzocatel  9944  fzostep1  9982  qtri3or  9988  qltnle  9991  qdceq  9992  exbtwnzlemex  9995  rebtwn2zlemstep  9998  rebtwn2z  10000  qbtwnxr  10003  ioom  10006  ico0  10007  ioc0  10008  flqeqceilz  10059  modqadd1  10102  modqmul1  10118  frec2uzuzd  10143  frec2uzlt2d  10145  frec2uzf1od  10147  frecuzrdgrrn  10149  frec2uzrdg  10150  frecuzrdgrcl  10151  frecuzrdgsuc  10155  frecuzrdgrclt  10156  frecuzrdgdomlem  10158  uzsinds  10183  seqvalcd  10200  seqovcd  10204  seq3fveq2  10210  seq3shft2  10214  monoord  10217  seq3split  10220  seq3caopr3  10222  iseqf1olemab  10230  iseqf1olemnanb  10231  iseqf1olemqk  10235  seq3id3  10248  seq3id2  10250  seq3homo  10251  expgt1  10299  m1expeven  10308  expnbnd  10383  expnlbnd2  10385  hashennn  10494  zfz1isolem1  10551  seq3coll  10553  cjap  10646  caucvgre  10721  cvg1nlemres  10725  resqrexlemgt0  10760  resqrexlemglsq  10762  resqrexlemga  10763  resqrtcl  10769  abslt  10828  abssubap0  10830  abssubne0  10831  caubnd2  10857  qdenre  10942  maxabslemlub  10947  maxabs  10949  maxleast  10953  fimaxre2  10966  xrmaxiflemlub  10985  xrmaxif  10988  xrmaxltsup  10995  xrmaxadd  10998  xrmineqinf  11006  climuni  11030  2clim  11038  climcn1  11045  climcn2  11046  subcn2  11048  mulcn2  11049  climsqz  11072  climsqz2  11073  climcau  11084  climcvg1nlem  11086  climcaucn  11088  serf0  11089  sumrbdclem  11113  summodclem2  11119  zsumdc  11121  divcnv  11234  absltap  11246  absgtap  11247  mertenslem2  11273  efcllemp  11291  tanvalap  11342  sin01bnd  11391  cos01bnd  11392  sin01gt0  11395  absef  11403  eirrap  11411  dvds0  11435  dvdsmul1  11442  dvdsmultr1d  11459  dvdslelemd  11468  divconjdvds  11474  alzdvds  11479  sqoddm1div8z  11510  nno  11530  divalglemex  11546  zsupcllemstep  11565  zsupcl  11567  infssuzledc  11570  dvdsbnd  11572  dvdslegcd  11580  zeqzmulgcd  11586  gcd0id  11594  gcdaddm  11599  gcd1  11602  gcdabs  11603  bezoutlemnewy  11611  bezoutlemstep  11612  bezoutlemmain  11613  bezoutlemex  11616  bezoutlemzz  11617  bezoutlemaz  11618  bezoutlembz  11619  bezoutlembi  11620  bezoutlemle  11623  bezoutlemsup  11624  mulgcd  11631  gcdzeq  11637  dvdsmulgcd  11640  sqgcd  11644  bezoutr1  11648  algcvga  11659  algfx  11660  eucalglt  11665  eucalg  11667  lcmneg  11682  lcmabs  11684  lcmgcdlem  11685  ncoprmgcdne1b  11697  mulgcddvds  11702  qredeq  11704  divgcdcoprm0  11709  cncongr1  11711  isprm2lem  11724  nprm  11731  dvdsnprmd  11733  prmdvdsfz  11746  coprm  11749  isprm6  11752  sqrt2irr  11767  pw2dvdslemn  11770  pw2dvdseulemle  11772  oddpwdclemdvds  11775  oddpwdclemndvds  11776  sqrt2irrap  11785  qnumdencl  11792  ennnfonelemex  11854  ennnfonelemhom  11855  ennnfonelemrnh  11856  ennnfonelemnn0  11862  ennnfonelemim  11864  exmidunben  11866  ctinfomlemom  11867  ctinfom  11868  ctinf  11870  tgcl  12160  neii1  12243  neii2  12245  neiss  12246  tpnei  12256  tgrest  12265  ssrest  12278  icnpimaex  12307  lmcvg  12313  cnpnei  12315  cnptopco  12318  lmff  12345  txcnp  12367  txcn  12371  hmeontr  12409  blssec  12534  mopni3  12580  blsscls2  12589  comet  12595  bdxmet  12597  bdmopn  12600  xmettxlem  12605  xmettx  12606  addcncntoplem  12647  mulc1cncf  12672  cncfco  12674  cncfmptc  12678  mulcncflem  12686  mulcncf  12687  dedekindeulemlu  12695  dedekindeulemeu  12696  suplociccreex  12698  suplociccex  12699  dedekindicclemlu  12704  dedekindicclemeu  12705  ivthinclemlopn  12710  ivthinclemlr  12711  ivthinclemuopn  12712  ivthinclemur  12713  ivthinclemloc  12715  ivthinc  12717  limcimolemlt  12729  limcresi  12731  cnplimcim  12732  cnplimclemle  12733  cnplimclemr  12734  limccnpcntop  12740  limccoap  12743  dvcoapbr  12767  dvcj  12769  sin0pilem2  12790  tangtx  12846  bj-exlimmpi  12904  uzdcinzz  12932  bj-2inf  13063  bj-peano4  13080  bj-nn0suc  13089  exmid1stab  13122  subctctexmid  13123  nninfalllem1  13130  nninfsellemqall  13138  nninfomnilem  13141  nninffeq  13143  exmidsbthrlem  13144  sbthomlem  13147  refeq  13150  isomninnlem  13152
  Copyright terms: Public domain W3C validator