ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpdan Structured version   GIF version

Theorem mpdan 398
Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
Hypotheses
Ref Expression
mpdan.1 (φψ)
mpdan.2 ((φ ψ) → χ)
Assertion
Ref Expression
mpdan (φχ)

Proof of Theorem mpdan
StepHypRef Expression
1 id 19 . 2 (φφ)
2 mpdan.1 . 2 (φψ)
3 mpdan.2 . 2 ((φ ψ) → χ)
41, 2, 3syl2anc 391 1 (φχ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  mpan2  401  mpjaodan  710  mpd3an3  1232  eueq2dc  2708  csbiegf  2884  difsnb  3497  reusv3i  4157  fvmpt3  5194  ffvelrnd  5246  fnressn  5292  fliftel1  5377  f1oiso2  5409  riota5f  5435  1stvalg  5711  2ndvalg  5712  brtpos2  5807  tfrlemibxssdm  5882  dom2lem  6188  nnfi  6251  recidnq  6377  archnqq  6400  prarloclemarch2  6402  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1l  6606  recexprlemss1u  6607  recexprlemex  6608  0idsr  6675  lep1  7572  uz11  8251  eluzfz2  8646  fzsuc  8681  fzsuc2  8691  fzp1disj  8692  fzneuz  8713  fzp1nel  8716  frecuzrdgsuc  8862  iseqcl  8883  iseqp1  8884  expubnd  8945  cjval  9053  reval  9057  imval  9058  cjmulrcl  9095  addcj  9099  absval  9190  absneg  9199  abscj  9200  bj-findis  9409
  Copyright terms: Public domain W3C validator