![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpr1 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpr1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 982 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantl 275 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: simplr1 1024 simprr1 1030 simp1r1 1078 simp2r1 1084 simp3r1 1090 3anandis 1326 isopolem 5731 caovlem2d 5971 tfrlemibacc 6231 tfrlemibfn 6233 tfr1onlembacc 6247 tfr1onlembfn 6249 tfrcllembacc 6260 tfrcllembfn 6262 eqsupti 6891 prmuloc2 7399 ltntri 7914 elioc2 9749 elico2 9750 elicc2 9751 fseq1p1m1 9905 elfz0ubfz0 9933 ico0 10070 seq3f1olemp 10306 seq3f1oleml 10307 bcval5 10541 isumss2 11194 tanaddap 11482 dvds2ln 11562 divalglemeunn 11654 divalglemex 11655 divalglemeuneg 11656 qredeq 11813 isstructr 12013 icnpimaex 12419 cnptopresti 12446 upxp 12480 psmettri 12538 isxmet2d 12556 xmettri 12580 metrtri 12585 xmetres2 12587 bldisj 12609 blss2ps 12614 blss2 12615 xmstri2 12678 mstri2 12679 xmstri 12680 mstri 12681 xmstri3 12682 mstri3 12683 msrtri 12684 comet 12707 bdbl 12711 xmetxp 12715 dvconst 12869 findset 13314 |
Copyright terms: Public domain | W3C validator |