ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpd Structured version   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  32  mpdd  36  mp2d  41  pm2.43i  43  syl3c  57  mpbid  135  mpbird  156  jcai  294  mp2and  409  pm2.21dd  535  mt2d  540  mpjaod  622  impidc  739  jadc  744  pm2.54dc  774  stabtestimpdc  808  pm4.55dc  828  oplem1  864  xor3dc  1256  exlimdd  1725  exlimddv  1751  eqrdav  2012  necon1aidc  2225  necon1bidc  2226  necon4aidc  2242  rexlimddv  2406  vtoclgft  2572  sseldd  2914  ssneldd  2916  tpid3g  3446  preq12b  3504  axpweq  3887  opth  3937  issod  4019  ralxfr2d  4134  rexxfr2d  4135  eldifpw  4146  onun2  4154  onuni  4158  elirr  4196  en2lp  4204  peano2  4233  relop  4401  elres  4561  sotri2  4637  iota4an  4801  iota5  4802  funeu  4840  funopg  4848  imadiflem  4892  funimaexglem  4896  ssimaex  5147  ffvelrn  5213  dff3im  5225  dffo4  5228  f1eqcocnv  5344  f1oiso2  5379  riota5f  5404  riotass2  5406  acexmidlemcase  5419  ovmpt2df  5543  ovmpt2dv2  5545  ovi3  5548  ov6g  5549  caoftrn  5647  op1steq  5716  tfrlemibxssdm  5850  tfrlemi14d  5856  rdgivallem  5876  frec0g  5890  frecsuclem3  5894  nnsucelsuc  5973  nnsucsssuc  5974  nnawordex  6000  ersym  6017  elni2  6160  mulclpi  6174  nlt1pig  6187  recclnq  6237  ltexnqq  6252  halfnqq  6253  prarloclemarch  6261  prarloclemarch2  6262  prop  6315  prltlu  6327  prnmaddl  6330  prarloclem3step  6336  prarloclem5  6340  prarloclem  6341  prarloc  6343  prarloc2  6344  genpml  6358  genpmu  6359  genprndl  6362  genprndu  6363  genpdisj  6364  addnqprllem  6368  addnqprulem  6369  addlocprlemeq  6374  addlocprlemgt  6375  addlocprlem  6376  addlocpr  6377  nqprloc  6386  appdivnq  6393  prmuloc  6396  prmuloc2  6397  mullocprlem  6400  mullocpr  6401  ltprordil  6414  ltpopr  6418  ltsopr  6419  ltaddpr  6420  ltexprlemm  6423  ltexprlemopl  6424  ltexprlemlol  6425  ltexprlemopu  6426  ltexprlemupu  6427  ltexprlemloc  6430  ltexprlemfl  6432  ltexprlemrl  6433  ltexprlemfu  6434  ltexprlemru  6435  ltaprg  6441  recexprlemm  6445  recexprlem1ssl  6454  recexprlem1ssu  6455  aptiprleml  6460  aptiprlemu  6461  recexgt0sr  6511  mulgt0sr  6514  lelttr  6706  ltletr  6707  ltled  6735  cnegexlem1  6786  cnegexlem2  6787  renegcl  6871  gt0add  7160  apreap  7174  apirr  7192  apsym  7193  apcotr  7194  apadd1  7195  apneg  7198  mulext1  7199  mulap0r  7202  apti  7209  recexap  7219  mulap0  7220  receuap  7235  lep1  7394  lem1  7396  letrp1  7397  recreclt  7449  nnrecgt0  7534  nn0ge2m1nn  7816  elnn0z  7832  peano2z  7854  zaddcl  7858  ztri3or0  7860  zltnle  7862  zdceq  7883  zdiv  7892  zeo  7907  fnn0ind  7918  qapne  8056  bj-exlimmpi  8175  bj-2inf  8322  bj-peano4  8339  bj-nn0suc  8344
  Copyright terms: Public domain W3C validator