![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > simpl12 | Structured version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl12 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp12 1019 |
. 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: pythagtriplem4 14005 brbtwn2 23304 ax5seg 23337 br8 27711 ifscgr 28220 seglecgr12im 28286 pmatcollpw1lem1 31262 pmatcollpw1 31264 mp2pm2mplem2 31295 lkrshp 33089 atlatle 33304 cvlcvr1 33323 atbtwn 33429 3dimlem3 33444 3dimlem3OLDN 33445 1cvratex 33456 llnmlplnN 33522 4atlem3 33579 4atlem3a 33580 4atlem11 33592 4atlem12 33595 cdlemb 33777 paddasslem4 33806 paddasslem10 33812 pmodlem1 33829 llnexchb2lem 33851 arglem1N 34173 cdlemd4 34184 cdlemd 34190 cdleme16 34268 cdleme20 34307 cdleme21k 34321 cdleme22cN 34325 cdleme27N 34352 cdleme28c 34355 cdleme29ex 34357 cdleme32fva 34420 cdleme40n 34451 cdlemg15a 34638 cdlemg15 34639 cdlemg16ALTN 34641 cdlemg16z 34642 cdlemg20 34668 cdlemg22 34670 cdlemg29 34688 cdlemg38 34698 cdlemk33N 34892 cdlemk56 34954 |
Copyright terms: Public domain | W3C validator |