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

Theorem simp3l 983
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3l ((φ ψ (χ θ)) → χ)

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 443 . 2 ((χ θ) → χ)
213ad2ant3 978 1 ((φ ψ (χ θ)) → χ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358   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:  simpl3l  1010  simpr3l  1016  simp13l  1070  simp23l  1076  simp33l  1082  nnpw1ex  4484  tfinpw1  4494  tfinltfinlem1  4500  nnadjoin  4520  nnpweq  4523  sfin112  4529  sfindbl  4530  sfintfin  4532  sfinltfin  4535  funprgOLD  5150  fvopab4t  5385
  Copyright terms: Public domain W3C validator