![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simp132 | Structured version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp132 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp32 1025 |
. 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 23324 3atlem1 33446 3atlem2 33447 3atlem5 33450 2llnjaN 33529 4atlem11b 33571 4atlem12b 33574 lplncvrlvol2 33578 dalemtea 33593 dath2 33700 cdlemblem 33756 dalawlem1 33834 lhpexle3lem 33974 4atexlemex6 34037 cdleme22f2 34310 cdleme22g 34311 cdlemg7aN 34588 cdlemg34 34675 cdlemj1 34784 cdlemk23-3 34865 cdlemk25-3 34867 cdlemk26b-3 34868 |
Copyright terms: Public domain | W3C validator |