Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp32r | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp32r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2r 1088 | . 2 | |
2 | 1 | 3ad2ant3 1084 | 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: cdlema1N 35077 paddasslem15 35120 4atex2-0aOLDN 35364 4atex3 35367 cdleme19b 35592 cdleme19d 35594 cdleme19e 35595 cdleme20d 35600 cdleme20f 35602 cdleme20g 35603 cdleme21d 35618 cdleme21e 35619 cdleme22cN 35630 cdleme22e 35632 cdleme22f2 35635 cdleme26e 35647 cdleme28a 35658 cdleme37m 35750 cdlemg28b 35991 cdlemk3 36121 cdlemk12 36138 cdlemk12u 36160 cdlemkoatnle-2N 36163 cdlemk13-2N 36164 cdlemkole-2N 36165 cdlemk14-2N 36166 cdlemk15-2N 36167 cdlemk16-2N 36168 cdlemk17-2N 36169 cdlemk18-2N 36174 cdlemk19-2N 36175 cdlemk7u-2N 36176 cdlemk11u-2N 36177 cdlemk20-2N 36180 cdlemk30 36182 cdlemk23-3 36190 cdlemk24-3 36191 |
Copyright terms: Public domain | W3C validator |