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  872  xor3dc  1258  exlimdd  1735  exlimddv  1761  eqrdav  2021  necon1aidc  2232  necon1bidc  2233  necon4aidc  2249  rexlimddv  2413  vtoclgft  2579  sseldd  2924  ssneldd  2926  tpid3g  3434  preq12b  3493  axpweq  3876  opth  3926  ralxfr2d  4119  rexxfr2d  4120  eldifpw  4131  onun2  4139  onuni  4143  elirr  4178  en2lp  4186  peano2  4214  relop  4379  elres  4540  sotri2  4616  iota4an  4780  iota5  4781  funeu  4819  funopg  4827  imadiflem  4871  funimaexglem  4875  ssimaex  5126  ffvelrn  5192  dff3im  5204  dffo4  5207  f1eqcocnv  5323  f1oiso2  5358  riota5f  5384  riotass2  5386  acexmidlemcase  5400  ovmpt2df  5524  ovmpt2dv2  5526  ov6g  5530  caoftrn  5625  op1steq  5694  tfrlemibxssdm  5827  tfrlemi14d  5833  rdgivallem  5853  frec0g  5868  frecsuclem3  5872
  Copyright terms: Public domain W3C validator