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: wi 4 wa 103 w3a 963 |
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 1329 isopolem 5774 caovlem2d 6015 tfrlemibacc 6275 tfrlemibfn 6277 tfr1onlembacc 6291 tfr1onlembfn 6293 tfrcllembacc 6304 tfrcllembfn 6306 eqsupti 6942 prmuloc2 7489 ltntri 8007 elioc2 9846 elico2 9847 elicc2 9848 fseq1p1m1 10002 elfz0ubfz0 10033 ico0 10170 seq3f1olemp 10410 seq3f1oleml 10411 bcval5 10648 isumss2 11301 tanaddap 11647 dvds2ln 11731 divalglemeunn 11824 divalglemex 11825 divalglemeuneg 11826 qredeq 11988 isstructr 12275 icnpimaex 12681 cnptopresti 12708 upxp 12742 psmettri 12800 isxmet2d 12818 xmettri 12842 metrtri 12847 xmetres2 12849 bldisj 12871 blss2ps 12876 blss2 12877 xmstri2 12940 mstri2 12941 xmstri 12942 mstri 12943 xmstri3 12944 mstri3 12945 msrtri 12946 comet 12969 bdbl 12973 xmetxp 12977 dvconst 13131 findset 13591 |
Copyright terms: Public domain | W3C validator |