New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simprr | GIF version |
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.) |
Ref | Expression |
---|---|
simprr | ⊢ ((φ ∧ (ψ ∧ χ)) → χ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (χ → χ) | |
2 | 1 | ad2antll 709 | 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: simp1rr 1021 simp2rr 1025 simp3rr 1029 prepeano4 4451 preaddccan2 4455 tfinltfin 4501 tfinnn 4534 vfinspsslem1 4550 weds 5938 ertr 5954 erth 5968 enadj 6060 enprmaplem3 6078 nntccl 6170 sbthlem1 6203 sbthlem3 6205 sbth 6206 tlecg 6230 nchoicelem6 6294 nchoicelem8 6296 nchoicelem19 6307 nchoice 6308 |
Copyright terms: Public domain | W3C validator |