New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simpll | GIF version |
Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.) |
Ref | Expression |
---|---|
simpll | ⊢ (((φ ∧ ψ) ∧ χ) → φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (φ → φ) | |
2 | 1 | ad2antrr 706 | 1 ⊢ (((φ ∧ ψ) ∧ χ) → φ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
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 |
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 |