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 992 | . 2 | |
2 | 1 | adantl 275 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 973 |
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 975 |
This theorem is referenced by: simplr1 1034 simprr1 1040 simp1r1 1088 simp2r1 1094 simp3r1 1100 3anandis 1342 isopolem 5801 caovlem2d 6045 tfrlemibacc 6305 tfrlemibfn 6307 tfr1onlembacc 6321 tfr1onlembfn 6323 tfrcllembacc 6334 tfrcllembfn 6336 eqsupti 6973 prmuloc2 7529 ltntri 8047 elioc2 9893 elico2 9894 elicc2 9895 fseq1p1m1 10050 elfz0ubfz0 10081 ico0 10218 seq3f1olemp 10458 seq3f1oleml 10459 bcval5 10697 isumss2 11356 tanaddap 11702 dvds2ln 11786 divalglemeunn 11880 divalglemex 11881 divalglemeuneg 11882 qredeq 12050 pcdvdstr 12280 isstructr 12431 mndissubm 12697 icnpimaex 13005 cnptopresti 13032 upxp 13066 psmettri 13124 isxmet2d 13142 xmettri 13166 metrtri 13171 xmetres2 13173 bldisj 13195 blss2ps 13200 blss2 13201 xmstri2 13264 mstri2 13265 xmstri 13266 mstri 13267 xmstri3 13268 mstri3 13269 msrtri 13270 comet 13293 bdbl 13297 xmetxp 13301 dvconst 13455 findset 13980 |
Copyright terms: Public domain | W3C validator |