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

Theorem simpl1 958
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl1 (((φ ψ χ) θ) → φ)

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 955 . 2 ((φ ψ χ) → φ)
21adantr 451 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:  simpll1  994  simprl1  1000  simp1l1  1048  simp2l1  1054  simp3l1  1060  3anandirs  1284  rspc3ev  2965  nnsucelr  4428  tfinltfin  4501  sfindbl  4530  enadjlem1  6059  enadj  6060  enprmaplem5  6080  lemuc2  6254  lecadd2  6266
  Copyright terms: Public domain W3C validator