![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl12 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl12 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp12 1040 |
. 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 988 |
This theorem is referenced by: pythagtriplem4 14781 pmatcollpw1lem1 19810 pmatcollpw1 19812 mp2pm2mplem2 19843 brbtwn2 24947 ax5seg 24980 br8 30408 ifscgr 30823 seglecgr12im 30889 lkrshp 32683 atlatle 32898 cvlcvr1 32917 atbtwn 33023 3dimlem3 33038 3dimlem3OLDN 33039 1cvratex 33050 llnmlplnN 33116 4atlem3 33173 4atlem3a 33174 4atlem11 33186 4atlem12 33189 cdlemb 33371 paddasslem4 33400 paddasslem10 33406 pmodlem1 33423 llnexchb2lem 33445 arglem1N 33768 cdlemd4 33779 cdlemd 33785 cdleme16 33863 cdleme20 33903 cdleme21k 33917 cdleme22cN 33921 cdleme27N 33948 cdleme28c 33951 cdleme29ex 33953 cdleme32fva 34016 cdleme40n 34047 cdlemg15a 34234 cdlemg15 34235 cdlemg16ALTN 34237 cdlemg16z 34238 cdlemg20 34264 cdlemg22 34266 cdlemg29 34284 cdlemg38 34294 cdlemk33N 34488 cdlemk56 34550 fourierdlem77 38057 |
Copyright terms: Public domain | W3C validator |