![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simp121 | Structured version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp121 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp21 1021 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant1 1009 |
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 185 df-an 371 df-3an 967 |
This theorem is referenced by: ax5seglem3 23314 axpasch 23324 exatleN 33356 ps-2b 33434 3atlem1 33435 3atlem2 33436 3atlem4 33438 3atlem5 33439 3atlem6 33440 2llnjaN 33518 4atlem12b 33563 2lplnja 33571 dalempea 33578 dath2 33689 lneq2at 33730 llnexchb2 33821 dalawlem1 33823 osumcllem7N 33914 lhpexle3lem 33963 cdleme26ee 34312 cdlemg34 34664 cdlemg36 34666 cdlemj1 34773 cdlemj2 34774 cdlemk23-3 34854 cdlemk25-3 34856 cdlemk26b-3 34857 cdlemk26-3 34858 cdlemk27-3 34859 cdleml3N 34930 |
Copyright terms: Public domain | W3C validator |