![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp33l | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp33l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3l 1058 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant3 1053 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 190 df-an 378 df-3an 1009 |
This theorem is referenced by: totprob 29333 cdleme19b 33942 cdleme19d 33944 cdleme19e 33945 cdleme20h 33954 cdleme20l2 33959 cdleme20m 33961 cdleme21d 33968 cdleme21e 33969 cdleme22e 33982 cdleme22f2 33985 cdleme22g 33986 cdleme26e 33997 cdleme28a 34008 cdleme28b 34009 cdleme37m 34100 cdleme39n 34104 cdlemeg46gfre 34170 cdlemg28a 34331 cdlemg28b 34341 cdlemk3 34471 cdlemk5a 34473 cdlemk6 34475 cdlemkuat 34504 cdlemkid2 34562 |
Copyright terms: Public domain | W3C validator |