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  1735  exlimddv  1761  eqrdav  2022  necon1aidc  2233  necon1bidc  2234  necon4aidc  2250  rexlimddv  2414  vtoclgft  2580  sseldd  2922  ssneldd  2924  tpid3g  3456  preq12b  3514  axpweq  3897  opth  3947  issod  4029  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  5656  op1steq  5725  tfrlemibxssdm  5857  tfrlemi14d  5863  rdgivallem  5883  frec0g  5897  frecsuclem3  5901  nnsucelsuc  5980  nnsucsssuc  5981  nnawordex  6007  ersym  6024  elni2  6167  mulclpi  6180  nlt1pig  6193  recclnq  6243  ltexnqq  6253  halfnqq  6254  prarloclemarch  6262  prarloclemarch2  6263  prop  6314  prltlu  6326  prnmaddl  6328  prarloclem3step  6333  prarloclem5  6337  prarloclem  6338  prarloc  6340  genpml  6351  genprndl  6353  genpdisj  6354  bj-exlimmpi  6369  bj-2inf  6502  bj-peano4  6522
  Copyright terms: Public domain W3C validator