![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl11 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl11 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp11 1038 |
. 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 987 |
This theorem is referenced by: pythagtriplem4 14769 tsmsxp 21169 brbtwn2 24935 ax5seg 24968 br8 30396 btwndiff 30794 ifscgr 30811 seglecgr12im 30877 lkrshp 32671 cvlcvr1 32905 atbtwn 33011 3dimlem3 33026 3dimlem3OLDN 33027 1cvratex 33038 llnmlplnN 33104 4atlem3 33161 4atlem3a 33162 4atlem11 33174 4atlem12 33177 lnatexN 33344 cdlemb 33359 paddasslem4 33388 paddasslem10 33394 pmodlem1 33411 llnexchb2lem 33433 llnexchb2 33434 arglem1N 33756 cdlemd4 33767 cdlemd9 33772 cdlemd 33773 cdleme16 33851 cdleme20 33891 cdleme21i 33902 cdleme21k 33905 cdleme27N 33936 cdleme28c 33939 cdlemefrs29bpre0 33963 cdlemefrs29clN 33966 cdlemefrs32fva 33967 cdleme41sn3a 34000 cdleme32fva 34004 cdleme40n 34035 cdlemg12e 34214 cdlemg15a 34222 cdlemg15 34223 cdlemg16ALTN 34225 cdlemg16z 34226 cdlemg20 34252 cdlemg22 34254 cdlemg29 34272 cdlemg38 34282 cdlemk33N 34476 cdlemk56 34538 dihord11b 34790 dihord2pre 34793 dihord4 34826 fourierdlem77 38047 |
Copyright terms: Public domain | W3C validator |