![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpr3 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpr3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 1001 |
. 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: simplr3 1043 simprr3 1049 simp1r3 1097 simp2r3 1103 simp3r3 1109 3anandis 1358 isopolem 5844 tfrlemibacc 6351 tfrlemibxssdm 6352 tfrlemibfn 6353 tfr1onlembacc 6367 tfr1onlembxssdm 6368 tfr1onlembfn 6369 tfrcllembacc 6380 tfrcllembxssdm 6381 tfrcllembfn 6382 elfir 7002 prloc 7520 prmuloc2 7596 ltntri 8115 eluzuzle 9566 xlesubadd 9913 elioc2 9966 elico2 9967 elicc2 9968 fseq1p1m1 10124 seq3f1olemp 10533 seq3f1oleml 10534 bcval5 10775 hashdifpr 10832 isumss2 11433 tanaddap 11779 dvds2ln 11863 divalglemeunn 11958 divalglemex 11959 divalglemeuneg 11960 f1ovscpbl 12789 grpsubadd 13032 grpaddsubass 13034 grpsubsub4 13037 grppnpcan2 13038 grpnpncan 13039 grpnnncan2 13041 imasgrp2 13052 imasgrp 13053 mulgnndir 13091 mulgnn0dir 13092 mulgnnass 13097 mulgnn0ass 13098 mulgass 13099 issubg2m 13128 qusgrp 13171 kerf1ghm 13213 cmn32 13243 cmn12 13245 abladdsub 13254 ablsubsub23 13264 rngass 13293 imasrng 13310 srgdilem 13323 srgass 13325 ringdilem 13366 ringass 13370 ringrng 13390 imasring 13414 opprrng 13427 opprring 13429 mulgass3 13435 unitgrp 13466 dvrass 13489 dvrdir 13493 subrgunit 13586 issubrg2 13588 aprap 13602 lss1 13678 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 |