Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpl32 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl32 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp32 1098 | . 2 | |
2 | 1 | adantr 481 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: initoeu2lem2 16665 mulmarep1gsum2 20380 tsmsxp 21958 ax5seg 25818 elwwlks2ons3 26848 br8d 29422 br8 31646 cgrextend 32115 segconeq 32117 trisegint 32135 ifscgr 32151 cgrsub 32152 btwnxfr 32163 seglecgr12im 32217 segletr 32221 exatleN 34690 atbtwn 34732 3dim1 34753 3dim2 34754 2llnjaN 34852 4atlem10b 34891 4atlem11 34895 4atlem12 34898 2lplnj 34906 cdlemb 35080 paddasslem4 35109 pmodlem1 35132 4atex2 35363 trlval3 35474 arglem1N 35477 cdleme0moN 35512 cdleme17b 35574 cdleme20 35612 cdleme21j 35624 cdleme28c 35660 cdleme35h2 35745 cdleme38n 35752 cdlemg6c 35908 cdlemg6 35911 cdlemg7N 35914 cdlemg11a 35925 cdlemg12e 35935 cdlemg16 35945 cdlemg16ALTN 35946 cdlemg16zz 35948 cdlemg20 35973 cdlemg22 35975 cdlemg37 35977 cdlemg31d 35988 cdlemg29 35993 cdlemg33b 35995 cdlemg33 35999 cdlemg39 36004 cdlemg42 36017 cdlemk25-3 36192 |
Copyright terms: Public domain | W3C validator |