ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpdan 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  711  mpd3an3  1233  eueq2dc  2711  csbiegf  2887  difsnb  3503  reusv3i  4187  fvmpt3  5238  ffvelrnd  5290  fnressn  5336  fliftel1  5421  f1oiso2  5453  riota5f  5479  1stvalg  5756  2ndvalg  5757  brtpos2  5853  tfrlemibxssdm  5928  dom2lem  6239  php5  6308  nnfi  6320  onenon  6345  oncardval  6347  cardonle  6348  recidnq  6472  archnqq  6496  prarloclemarch2  6498  recexprlem1ssl  6712  recexprlem1ssu  6713  recexprlemss1l  6714  recexprlemss1u  6715  recexprlemex  6716  0idsr  6833  lep1  7787  uz11  8467  eluzfz2  8863  fzsuc  8898  fzsuc2  8908  fzp1disj  8909  fzneuz  8930  fzp1nel  8933  frecuzrdgsuc  9079  iseqcl  9101  iseqp1  9103  expubnd  9189  shftfval  9300  shftcan1  9313  cjval  9323  reval  9327  imval  9328  cjmulrcl  9365  addcj  9369  absval  9477  resqrexlemdecn  9488  resqrexlemnmsq  9493  resqrexlemnm  9494  absneg  9526  abscj  9528  sqabsadd  9531  sqabssub  9532  ltabs  9561  bj-findis  9977
  Copyright terms: Public domain W3C validator