New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simprl | GIF version |
Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.) |
Ref | Expression |
---|---|
simprl | ⊢ ((φ ∧ (ψ ∧ χ)) → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (ψ → ψ) | |
2 | 1 | ad2antrl 708 | 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: simp1rl 1020 simp2rl 1024 simp3rl 1028 rmob 3134 prepeano4 4451 preaddccan2 4455 tfin11 4493 tfinltfin 4501 evenodddisj 4516 sfindbl 4530 tfinnn 4534 vfinspsslem1 4550 vfinspclt 4552 xp0r 4842 weds 5938 ertr 5954 erth 5968 enadj 6060 enprmaplem3 6078 nntccl 6170 sbthlem3 6205 sbth 6206 tlecg 6230 nchoicelem6 6294 nchoicelem8 6296 nchoicelem19 6307 nchoice 6308 |
Copyright terms: Public domain | W3C validator |