![]() |
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 965 |
. 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 947 |
This theorem is referenced by: simplr2 1007 simprr2 1013 simp1r2 1061 simp2r2 1067 simp3r2 1073 3anandis 1308 isopolem 5677 tfrlemibacc 6177 tfrlemibfn 6179 tfr1onlembacc 6193 tfr1onlembfn 6195 tfrcllembacc 6206 tfrcllembfn 6208 prltlu 7243 prdisj 7248 prmuloc2 7323 ltntri 7813 eluzuzle 9236 xlesubadd 9559 elioc2 9612 elico2 9613 elicc2 9614 fseq1p1m1 9767 fz0fzelfz0 9797 seq3f1olemp 10168 bcval5 10402 hashdifpr 10459 summodclem2 11043 isumss2 11054 tanaddap 11297 dvds2ln 11374 divalglemeunn 11466 divalglemex 11467 divalglemeuneg 11468 isstructr 11817 restopnb 12193 icnpimaex 12222 cnptopresti 12249 psmettri 12319 isxmet2d 12337 xmettri 12361 metrtri 12366 xmetres2 12368 bldisj 12390 blss2ps 12395 blss2 12396 xmstri2 12459 mstri2 12460 xmstri 12461 mstri 12462 xmstri3 12463 mstri3 12464 msrtri 12465 comet 12488 bdbl 12492 xmetxp 12496 dvconst 12616 |
Copyright terms: Public domain | W3C validator |