New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simp2 | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
simp2 | ⊢ ((φ ∧ ψ ∧ χ) → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa 952 | . 2 ⊢ ((φ ∧ ψ ∧ χ) → (φ ∧ ψ)) | |
2 | 1 | simprd 449 | 1 ⊢ ((φ ∧ ψ ∧ χ) → ψ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ 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: simpl2 959 simpr2 962 simp2i 965 simp2d 968 simp12 986 simp22 989 simp32 992 syld3an3 1227 opkthg 4131 nnsucelrlem3 4426 ltfintri 4466 ncfindi 4475 sfintfin 4532 vfintle 4546 phi11lem1 4595 fvopab4t 5385 xpassen 6057 nenpw1pwlem2 6085 ceclnn1 6189 spacssnc 6284 spaccl 6286 nchoicelem17 6305 |
Copyright terms: Public domain | W3C validator |