![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simpl1 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 997 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 276 |
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 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: simpll1 1036 simprl1 1042 simp1l1 1090 simp2l1 1096 simp3l1 1102 3anandirs 1348 rspc3ev 2858 brcogw 4796 cocan1 5787 oawordi 6469 nnmord 6517 nnmword 6518 dif1en 6878 ac6sfi 6897 ordiso2 7033 difinfsn 7098 ctssdc 7111 2omotaplemap 7255 enq0tr 7432 distrlem4prl 7582 distrlem4pru 7583 ltaprg 7617 aptiprlemu 7638 lelttr 8045 readdcan 8096 addcan 8136 addcan2 8137 ltadd2 8375 ltmul1a 8547 ltmul1 8548 divmulassap 8651 divmulasscomap 8652 lemul1a 8814 xrlelttr 9805 xleadd1a 9872 xlesubadd 9882 icoshftf1o 9990 lincmb01cmp 10002 iccf1o 10003 fztri3or 10038 fzofzim 10187 ioom 10260 modqmuladdim 10366 modqm1p1mod0 10374 q2submod 10384 modqaddmulmod 10390 ltexp2a 10571 exple1 10575 expnlbnd2 10645 nn0ltexp2 10688 nn0leexp2 10689 expcan 10695 fiprsshashgt1 10796 fimaxq 10806 maxleastb 11222 maxltsup 11226 xrltmaxsup 11264 xrmaxltsup 11265 xrmaxaddlem 11267 addcn2 11317 mulcn2 11319 dvdsmodexp 11801 dvdsadd2b 11846 dvdsmod 11867 oexpneg 11881 divalglemex 11926 divalg 11928 gcdass 12015 rplpwr 12027 rppwr 12028 nnwodc 12036 coprmdvds2 12092 rpmulgcd2 12094 qredeq 12095 rpdvds 12098 cncongr2 12103 rpexp 12152 znege1 12177 prmdiveq 12235 hashgcdlem 12237 odzdvds 12244 modprmn0modprm0 12255 coprimeprodsq2 12257 pythagtriplem3 12266 pcdvdsb 12318 pcgcd1 12326 qexpz 12349 pockthg 12354 ctinf 12430 nninfdc 12453 unbendc 12454 isnsgrp 12811 issubmnd 12842 ress0g 12843 mulgneg 13000 mulgdirlem 13012 subgmulg 13046 nmzsubg 13068 srg1zr 13168 ring1eq0 13223 mulgass2 13233 neiint 13581 topssnei 13598 iscnp4 13654 cnptopco 13658 cnconst2 13669 cnrest2 13672 cnptoprest 13675 cnpdis 13678 bldisj 13837 blgt0 13838 bl2in 13839 blss2ps 13842 blss2 13843 xblm 13853 blssps 13863 blss 13864 xmetresbl 13876 bdbl 13939 metcnp3 13947 metcnp2 13949 cncfmptc 14018 dvcnp2cntop 14099 dvcn 14100 logdivlti 14238 ltexp2 14296 lgsfcl2 14343 lgsdilem 14364 lgsdirprm 14371 lgsdir 14372 lgsdi 14374 lgsne0 14375 |
Copyright terms: Public domain | W3C validator |