New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simp1 | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
simp1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa 952 | . 2 | |
2 | 1 | simpld 445 | 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: simpl1 958 simpr1 961 simp1i 964 simp1d 967 simp11 985 simp21 988 simp31 991 syld3an3 1227 rsp2e 2677 opkthg 4131 ltfintri 4466 ssfin 4470 foco2 5426 f1oiso2 5500 xpassen 6057 enadj 6060 lectr 6211 |
Copyright terms: Public domain | W3C validator |