Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpr32 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpr32 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp32 1098 | . 2 | |
2 | 1 | adantl 482 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: oppccatid 16379 subccatid 16506 fuccatid 16629 setccatid 16734 catccatid 16752 estrccatid 16772 xpccatid 16828 nllyidm 21292 utoptop 22038 omndmul2 29712 cgr3tr4 32159 paddasslem9 35114 cdlemd1 35485 cdlemf2 35850 cdlemk34 36198 dihmeetlem18N 36613 |
Copyright terms: Public domain | W3C validator |