Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp122 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp122 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp22 1095 | . 2 | |
2 | 1 | 3ad2ant1 1082 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 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: ax5seglem3 25811 axpasch 25821 exatleN 34690 ps-2b 34768 3atlem1 34769 3atlem2 34770 3atlem4 34772 3atlem5 34773 3atlem6 34774 2llnjaN 34852 4atlem12b 34897 2lplnja 34905 dalemqea 34913 dath2 35023 lneq2at 35064 llnexchb2 35155 dalawlem1 35157 lhpexle3lem 35297 cdleme26ee 35648 cdlemg34 36000 cdlemg35 36001 cdlemg36 36002 cdlemj1 36109 cdlemj2 36110 cdlemk23-3 36190 cdlemk25-3 36192 cdlemk26b-3 36193 cdlemk26-3 36194 cdleml3N 36266 |
Copyright terms: Public domain | W3C validator |