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

Theorem mp3an1 1264
 Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an1.1 φ
mp3an1.2 ((φ ψ χ) → θ)
Assertion
Ref Expression
mp3an1 ((ψ χ) → θ)

Proof of Theorem mp3an1
StepHypRef Expression
1 mp3an1.1 . 2 φ
2 mp3an1.2 . . 3 ((φ ψ χ) → θ)
323expb 1152 . 2 ((φ (ψ χ)) → θ)
41, 3mpan 651 1 ((ψ χ) → θ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936 This theorem is referenced by:  mp3an12  1267  mp3an1i  1270  mp3anl1  1271  mp3an  1277  opkelcokg  4261  opkelimagekg  4271  ltfintri  4466  vfinspnn  4541  vfinspclt  4552  spaccl  6286  spacind  6287  nchoicelem3  6291  nchoicelem4  6292  nchoicelem6  6294  nchoicelem9  6297  nchoicelem12  6300  nchoicelem14  6302  nchoicelem17  6305
 Copyright terms: Public domain W3C validator