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

Theorem mp3an 1277
 Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
Hypotheses
Ref Expression
mp3an.1 φ
mp3an.2 ψ
mp3an.3 χ
mp3an.4 ((φ ψ χ) → θ)
Assertion
Ref Expression
mp3an θ

Proof of Theorem mp3an
StepHypRef Expression
1 mp3an.2 . 2 ψ
2 mp3an.3 . 2 χ
3 mp3an.1 . . 3 φ
4 mp3an.4 . . 3 ((φ ψ χ) → θ)
53, 4mp3an1 1264 . 2 ((ψ χ) → θ)
61, 2, 5mp2an 653 1 θ
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 934 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  df-3an 936 This theorem is referenced by:  vtocl3  2911  raltp  3781  rextp  3782  opkth  4132  otkelins2k  4255  otkelins3k  4256  caovass  5627  caovdi  5634  oprabid2  5646  clos1is  5881  clos10  5887  elmap  6017  elpm  6019  elpm2  6020  xpassen  6057  tcdi  6164  ce0addcnnul  6179  tlenc1c  6240  ncvsq  6256  nchoicelem9  6297  frecxp  6314
 Copyright terms: Public domain W3C validator