![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simpl32 | Structured version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl32 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp32 1025 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 465 |
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: tsmsxp 19854 ax5seg 23329 br8d 26086 br8 27703 cgrextend 28176 segconeq 28178 trisegint 28196 ifscgr 28212 cgrsub 28213 btwnxfr 28224 seglecgr12im 28278 segletr 28282 exatleN 33357 atbtwn 33399 3dim1 33420 3dim2 33421 2llnjaN 33519 4atlem10b 33558 4atlem11 33562 4atlem12 33565 2lplnj 33573 cdlemb 33747 paddasslem4 33776 pmodlem1 33799 4atex2 34030 trlval3 34140 arglem1N 34143 cdleme0moN 34178 cdleme17b 34240 cdleme20 34277 cdleme21j 34289 cdleme28c 34325 cdleme35h2 34410 cdleme38n 34417 cdlemg6c 34573 cdlemg6 34576 cdlemg7N 34579 cdlemg11a 34590 cdlemg12e 34600 cdlemg16 34610 cdlemg16ALTN 34611 cdlemg16zz 34613 cdlemg20 34638 cdlemg22 34640 cdlemg37 34642 cdlemg31d 34653 cdlemg29 34658 cdlemg33b 34660 cdlemg33 34664 cdlemg39 34669 cdlemg42 34682 cdlemk25-3 34857 |
Copyright terms: Public domain | W3C validator |