Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpl2 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 993 | . 2 | |
2 | 1 | adantr 274 | 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 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: simpll2 1032 simprl2 1038 simp1l2 1086 simp2l2 1092 simp3l2 1098 3anandirs 1343 rspc3ev 2851 tfisi 4571 brcogw 4780 oawordi 6448 nnmord 6496 nnmword 6497 ac6sfi 6876 unsnfi 6896 unsnfidcel 6898 ordiso2 7012 prarloclemarch2 7381 enq0tr 7396 distrlem4prl 7546 distrlem4pru 7547 ltaprg 7581 aptiprlemu 7602 lelttr 8008 ltletr 8009 readdcan 8059 addcan 8099 addcan2 8100 ltadd2 8338 ltmul1a 8510 ltmul1 8511 divmulassap 8612 divmulasscomap 8613 lemul1a 8774 xrlelttr 9763 xrltletr 9764 xaddass 9826 xleadd1a 9830 xltadd1 9833 xlesubadd 9840 ixxdisj 9860 icoshftf1o 9948 icodisj 9949 lincmb01cmp 9960 iccf1o 9961 fztri3or 9995 ioom 10217 modqmuladdim 10323 modqmuladdnn0 10324 q2submod 10341 modqaddmulmod 10347 exp3val 10478 ltexp2a 10528 exple1 10532 expnbnd 10599 expnlbnd2 10601 nn0ltexp2 10644 nn0leexp2 10645 expcan 10650 fiprsshashgt1 10752 maxleastb 11178 maxltsup 11182 xrltmaxsup 11220 xrmaxltsup 11221 xrmaxaddlem 11223 xrmaxadd 11224 addcn2 11273 mulcn2 11275 geoisum1c 11483 dvdsval2 11752 dvdsmodexp 11757 dvdsadd2b 11802 dvdsmod 11822 oexpneg 11836 divalglemex 11881 divalg 11883 gcdass 11970 rplpwr 11982 rppwr 11983 nnminle 11990 lcmass 12039 coprmdvds2 12047 rpmulgcd2 12049 rpdvds 12053 cncongr2 12058 rpexp 12107 znege1 12132 prmdiveq 12190 hashgcdlem 12192 odzdvds 12199 coprimeprodsq2 12212 pythagtriplem3 12221 pythagtriplem4 12222 pcdvdsb 12273 pcbc 12303 ctinf 12385 nninfdc 12408 isnsgrp 12647 topssnei 12956 cnptopco 13016 cnconst2 13027 cnptoprest 13033 cnpdis 13036 upxp 13066 bldisj 13195 blgt0 13196 bl2in 13197 blss2ps 13200 blss2 13201 xblm 13211 blssps 13221 blss 13222 xmetresbl 13234 bdbl 13297 bdmopn 13298 metcnp3 13305 metcnp 13306 metcnp2 13307 dvfvalap 13444 dvcnp2cntop 13457 dvcn 13458 logdivlti 13596 ltexp2 13654 lgsfvalg 13700 lgsneg 13719 lgsdilem 13722 lgsdirprm 13729 lgsdir 13730 lgsdi 13732 lgsne0 13733 |
Copyright terms: Public domain | W3C validator |