![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl33 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl33 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp33 1045 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 467 |
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 189 df-an 373 df-3an 986 |
This theorem is referenced by: ax5seglem3a 24953 ax5seg 24961 br8d 28211 br8 30389 cgrextend 30768 segconeq 30770 trisegint 30788 ifscgr 30804 cgrsub 30805 btwnxfr 30816 seglecgr12im 30870 segletr 30874 atbtwn 33005 4atlem10b 33164 4atlem11 33168 4atlem12 33171 2lplnj 33179 paddasslem4 33382 paddasslem7 33385 pmodlem1 33405 4atex2 33636 trlval3 33747 arglem1N 33750 cdleme0moN 33785 cdleme20 33885 cdleme21j 33897 cdleme28c 33933 cdleme38n 34025 cdlemg6c 34181 cdlemg6 34184 cdlemg7N 34187 cdlemg16 34218 cdlemg16ALTN 34219 cdlemg16zz 34221 cdlemg20 34246 cdlemg22 34248 cdlemg37 34250 cdlemg31d 34261 cdlemg29 34266 cdlemg33b 34268 cdlemg33 34272 cdlemg46 34296 cdlemk25-3 34465 |
Copyright terms: Public domain | W3C validator |