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

Theorem simpll 730
Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
Assertion
Ref Expression
simpll (((φ ψ) χ) → φ)

Proof of Theorem simpll
StepHypRef Expression
1 id 19 . 2 (φφ)
21ad2antrr 706 1 (((φ ψ) χ) → φ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
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
This theorem is referenced by:  simp1ll  1018  simp2ll  1022  simp3ll  1026  pm2.61da3ne  2596  rmob  3134  ifboth  3693  nndisjeq  4429  preaddccan2  4455  ltfinirr  4457  lenltfin  4469  sfintfin  4532  tfinnn  4534  imainss  5042  ncdisjun  6136  sbth  6206  leconnnc  6218  tlecg  6230  lemuc1  6253  nchoicelem4  6292  nchoicelem19  6307  nchoice  6308
  Copyright terms: Public domain W3C validator