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  6603  recexprlem1ssu  6604  recexprlemss1l  6605  recexprlemss1u  6606  recexprlemex  6607  0idsr  6655  lep1  7552  uz11  8231  eluzfz2  8626  fzsuc  8661  fzsuc2  8671  fzp1disj  8672  fzneuz  8693  fzp1nel  8696  frecuzrdgsuc  8842  iseqcl  8863  iseqp1  8864  expubnd  8925  cjval  9033  reval  9037  imval  9038  cjmulrcl  9075  addcj  9079  bj-findis  9363
  Copyright terms: Public domain W3C validator