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 983 | . 2 | |
2 | 1 | adantl 275 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
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 964 |
This theorem is referenced by: simplr3 1025 simprr3 1031 simp1r3 1079 simp2r3 1085 simp3r3 1091 3anandis 1325 isopolem 5723 tfrlemibacc 6223 tfrlemibxssdm 6224 tfrlemibfn 6225 tfr1onlembacc 6239 tfr1onlembxssdm 6240 tfr1onlembfn 6241 tfrcllembacc 6252 tfrcllembxssdm 6253 tfrcllembfn 6254 elfir 6861 prloc 7299 prmuloc2 7375 ltntri 7890 eluzuzle 9334 xlesubadd 9666 elioc2 9719 elico2 9720 elicc2 9721 fseq1p1m1 9874 seq3f1olemp 10275 seq3f1oleml 10276 bcval5 10509 hashdifpr 10566 isumss2 11162 tanaddap 11446 dvds2ln 11526 divalglemeunn 11618 divalglemex 11619 divalglemeuneg 11620 restopnb 12350 icnpimaex 12380 cnptopresti 12407 psmettri 12499 isxmet2d 12517 xmettri 12541 metrtri 12546 xmetres2 12548 bldisj 12570 blss2ps 12575 blss2 12576 xmstri2 12639 mstri2 12640 xmstri 12641 mstri 12642 xmstri3 12643 mstri3 12644 msrtri 12645 comet 12668 bdbl 12672 xmetxp 12676 dvconst 12830 |
Copyright terms: Public domain | W3C validator |