![]() |
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 999 |
. 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 980 |
This theorem is referenced by: simplr3 1041 simprr3 1047 simp1r3 1095 simp2r3 1101 simp3r3 1107 3anandis 1347 isopolem 5817 tfrlemibacc 6321 tfrlemibxssdm 6322 tfrlemibfn 6323 tfr1onlembacc 6337 tfr1onlembxssdm 6338 tfr1onlembfn 6339 tfrcllembacc 6350 tfrcllembxssdm 6351 tfrcllembfn 6352 elfir 6966 prloc 7478 prmuloc2 7554 ltntri 8072 eluzuzle 9522 xlesubadd 9867 elioc2 9920 elico2 9921 elicc2 9922 fseq1p1m1 10077 seq3f1olemp 10485 seq3f1oleml 10486 bcval5 10724 hashdifpr 10781 isumss2 11382 tanaddap 11728 dvds2ln 11812 divalglemeunn 11906 divalglemex 11907 divalglemeuneg 11908 grpsubadd 12844 grpaddsubass 12846 grpsubsub4 12849 grppnpcan2 12850 grpnpncan 12851 grpnnncan2 12853 mulgnndir 12897 mulgnn0dir 12898 mulgnnass 12903 mulgnn0ass 12904 mulgass 12905 cmn32 12931 cmn12 12933 abladdsub 12942 ablsubsub23 12952 srgdilem 12975 srgass 12977 ringdilem 13018 ringass 13022 opprring 13071 mulgass3 13076 unitgrp 13107 dvrass 13130 restopnb 13341 icnpimaex 13371 cnptopresti 13398 psmettri 13490 isxmet2d 13508 xmettri 13532 metrtri 13537 xmetres2 13539 bldisj 13561 blss2ps 13566 blss2 13567 xmstri2 13630 mstri2 13631 xmstri 13632 mstri 13633 xmstri3 13634 mstri3 13635 msrtri 13636 comet 13659 bdbl 13663 xmetxp 13667 dvconst 13821 |
Copyright terms: Public domain | W3C validator |