Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp33r | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp33r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3r 1090 | . 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: totprob 30489 cdleme19b 35592 cdleme19e 35595 cdleme20h 35604 cdleme20l2 35609 cdleme20m 35611 cdleme21d 35618 cdleme21e 35619 cdleme22eALTN 35633 cdleme22f2 35635 cdleme22g 35636 cdleme26e 35647 cdleme37m 35750 cdlemeg46gfre 35820 cdlemg28a 35981 cdlemg28b 35991 cdlemk5a 36123 cdlemk6 36125 |
Copyright terms: Public domain | W3C validator |