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  411  pm2.21dd  538  mt2d  543  mpjaod  625  stabtestimpdc  745  impidc  748  jadc  753  pm2.54dc  783  pm4.55dc  834  oplem1  870  xor3dc  1261  exlimdd  1734  exlimddv  1760  eqrdav  2021  necon1aidc  2232  necon1bidc  2233  necon4aidc  2249  rexlimddv  2413  vtoclgft  2579  sseldd  2921  ssneldd  2923  tpid3g  3455  preq12b  3513  axpweq  3896  opth  3946  issod  4028  ralxfr2d  4144  rexxfr2d  4145  eldifpw  4156  onun2  4164  onuni  4168  elirr  4206  en2lp  4214  peano2  4243  relop  4411  elres  4571  sotri2  4647  iota4an  4811  iota5  4812  funeu  4850  funopg  4858  imadiflem  4902  funimaexglem  4906  ssimaex  5157  ffvelrn  5223  dff3im  5235  dffo4  5238  f1eqcocnv  5354  f1oiso2  5389  riota5f  5414  riotass2  5416  acexmidlemcase  5429  ovmpt2df  5553  ovmpt2dv2  5555  ovi3  5558  ov6g  5559  caoftrn  5657  op1steq  5726  tfrlemibxssdm  5860  tfrlemi14d  5866  rdgivallem  5886  frec0g  5900  frecsuclem3  5904  nnsucelsuc  5983  nnsucsssuc  5984  nnawordex  6010  ersym  6027  elni2  6172  mulclpi  6186  nlt1pig  6199  recclnq  6249  ltexnqq  6264  halfnqq  6265  prarloclemarch  6273  prarloclemarch2  6274  prop  6327  prltlu  6339  prnmaddl  6342  prarloclem3step  6348  prarloclem5  6352  prarloclem  6353  prarloc  6355  prarloc2  6356  genpml  6370  genpmu  6371  genprndl  6374  genprndu  6375  genpdisj  6376  addnqprllem  6380  addnqprulem  6381  addlocprlemeq  6386  addlocprlemgt  6387  addlocprlem  6388  addlocpr  6389  nqprloc  6398  appdivnq  6405  prmuloc  6408  prmuloc2  6409  mullocprlem  6412  mullocpr  6413  ltprordil  6426  ltpopr  6430  ltsopr  6431  ltaddpr  6432  ltexprlemm  6435  ltexprlemopl  6436  ltexprlemlol  6437  ltexprlemopu  6438  ltexprlemupu  6439  ltexprlemloc  6442  ltexprlemfl  6444  ltexprlemrl  6445  ltexprlemfu  6446  ltexprlemru  6447  addcanprleml  6449  ltaprg  6453  recexprlemm  6456  recexprlem1ssl  6465  recexprlem1ssu  6466  recexsrlem  6518  mulgt0sr  6520  bj-exlimmpi  6696  bj-2inf  6839  bj-peano4  6856  bj-nn0suc  6861
  Copyright terms: Public domain W3C validator