New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpdan GIF version

Theorem mpdan 649
 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 642 1 (φχ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  mpan2  652  mpjaodan  761  mpd3an3  1278  eueq2  3010  csbiegf  3176  difsnb  3850  ltfinp1  4462  vfinncsp  4554  addccan2  4559  fnressn  5438  f1oiso2  5500  fvdomfn  5868  fvranfn  5869  qsdisj  5995  enadj  6060  enmap2lem3  6065  enmap1lem3  6071  nclecid  6197  le0nc  6200  nnltp1c  6262  nmembers1  6271
 Copyright terms: Public domain W3C validator