![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpr2 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpr2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 1000 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantl 277 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: simplr2 1042 simprr2 1048 simp1r2 1096 simp2r2 1102 simp3r2 1108 3anandis 1358 isopolem 5844 tfrlemibacc 6351 tfrlemibfn 6353 tfr1onlembacc 6367 tfr1onlembfn 6369 tfrcllembacc 6380 tfrcllembfn 6382 prltlu 7516 prdisj 7521 prmuloc2 7596 ltntri 8115 eluzuzle 9566 xlesubadd 9913 elioc2 9966 elico2 9967 elicc2 9968 fseq1p1m1 10124 fz0fzelfz0 10157 seq3f1olemp 10533 bcval5 10775 hashdifpr 10832 summodclem2 11422 isumss2 11433 tanaddap 11779 dvds2ln 11863 divalglemeunn 11958 divalglemex 11959 divalglemeuneg 11960 isstructr 12527 f1ovscpbl 12789 mndissubm 12927 grpsubrcan 13025 grpsubadd 13032 grpaddsubass 13034 grpsubsub4 13037 grppnpcan2 13038 grpnpncan 13039 mulgnndir 13091 mulgnn0dir 13092 mulgdir 13094 mulgnnass 13097 mulgnn0ass 13098 mulgass 13099 mulgsubdir 13102 issubg2m 13128 eqgval 13162 qusgrp 13171 cmn32 13243 cmn12 13245 abladdsub 13254 ablsubsub23 13264 rngass 13293 srgdilem 13323 srgass 13325 ringdilem 13366 ringass 13370 opprrng 13427 opprring 13429 mulgass3 13435 unitgrp 13466 dvrass 13489 dvrdir 13493 subrgunit 13586 issubrg2 13588 aprap 13602 lsssn0 13686 islss3 13695 sralmod 13766 restopnb 14141 icnpimaex 14171 cnptopresti 14198 psmettri 14290 isxmet2d 14308 xmettri 14332 metrtri 14337 xmetres2 14339 bldisj 14361 blss2ps 14366 blss2 14367 xmstri2 14430 mstri2 14431 xmstri 14432 mstri 14433 xmstri3 14434 mstri3 14435 msrtri 14436 comet 14459 bdbl 14463 xmetxp 14467 dvconst 14621 |
Copyright terms: Public domain | W3C validator |