Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpl3 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 988 | . 2 | |
2 | 1 | adantr 274 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 967 |
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 969 |
This theorem is referenced by: simpll3 1027 simprl3 1033 simp1l3 1081 simp2l3 1087 simp3l3 1093 3anandirs 1337 frirrg 4322 fcofo 5746 acexmid 5835 rdgon 6345 oawordi 6428 nnmord 6476 nnmword 6477 fidifsnen 6827 dif1en 6836 ac6sfi 6855 difinfsn 7056 enq0tr 7366 distrlem4prl 7516 distrlem4pru 7517 ltaprg 7551 lelttr 7978 ltletr 7979 readdcan 8029 addcan 8069 addcan2 8070 ltadd2 8308 divmulassap 8582 xrlelttr 9733 xrltletr 9734 xaddass 9796 xleadd1a 9800 xlesubadd 9810 icoshftf1o 9918 difelfzle 10059 fzo1fzo0n0 10108 modqmuladdim 10292 modqmuladdnn0 10293 modqm1p1mod0 10300 q2submod 10310 modifeq2int 10311 modqaddmulmod 10316 ltexp2a 10497 exple1 10501 expnlbnd2 10569 nn0ltexp2 10612 nn0leexp2 10613 expcan 10618 fiprsshashgt1 10719 maxleastb 11142 maxltsup 11146 xrltmaxsup 11184 xrmaxltsup 11185 xrmaxaddlem 11187 xrmaxadd 11188 addcn2 11237 mulcn2 11239 isumz 11316 dvdsmodexp 11721 modmulconst 11749 dvdsmod 11785 divalglemex 11844 divalg 11846 gcdass 11933 rplpwr 11945 rppwr 11946 rpmulgcd2 12006 rpdvds 12010 rpexp 12064 znege1 12089 prmdiveq 12147 hashgcdlem 12149 coprimeprodsq 12168 coprimeprodsq2 12169 pythagtriplem3 12178 pcdvdsb 12230 pcgcd1 12238 dvdsprmpweq 12245 pcbc 12260 ctinf 12306 nninfdc 12331 neiint 12692 topssnei 12709 cnptopco 12769 cnrest2 12783 cnptoprest 12786 upxp 12819 bldisj 12948 blgt0 12949 bl2in 12950 blss2ps 12953 blss2 12954 xblm 12964 blssps 12974 blss 12975 bdmopn 13051 metcnp2 13060 txmetcnp 13065 cncfmptc 13129 dvcnp2cntop 13210 dvcn 13211 logdivlti 13349 ltexp2 13407 |
Copyright terms: Public domain | W3C validator |