![]() |
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 951 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantl 273 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 932 |
This theorem is referenced by: simplr3 993 simprr3 999 simp1r3 1047 simp2r3 1053 simp3r3 1059 3anandis 1293 isopolem 5655 tfrlemibacc 6153 tfrlemibxssdm 6154 tfrlemibfn 6155 tfr1onlembacc 6169 tfr1onlembxssdm 6170 tfr1onlembfn 6171 tfrcllembacc 6182 tfrcllembxssdm 6183 tfrcllembfn 6184 prloc 7200 prmuloc2 7276 ltntri 7761 eluzuzle 9184 xlesubadd 9507 elioc2 9560 elico2 9561 elicc2 9562 fseq1p1m1 9715 seq3f1olemp 10116 seq3f1oleml 10117 bcval5 10350 hashdifpr 10407 isumss2 11001 tanaddap 11244 dvds2ln 11321 divalglemeunn 11413 divalglemex 11414 divalglemeuneg 11415 restopnb 12132 icnpimaex 12161 cnptopresti 12188 psmettri 12258 isxmet2d 12276 xmettri 12300 metrtri 12305 xmetres2 12307 bldisj 12329 blss2ps 12334 blss2 12335 xmstri2 12398 mstri2 12399 xmstri 12400 mstri 12401 xmstri3 12402 mstri3 12403 msrtri 12404 comet 12427 bdbl 12431 dvconst 12534 |
Copyright terms: Public domain | W3C validator |