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 983 | . 2 | |
2 | 1 | adantr 274 | 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 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: simpll2 1022 simprl2 1028 simp1l2 1076 simp2l2 1082 simp3l2 1088 3anandirs 1330 rspc3ev 2833 tfisi 4547 brcogw 4756 oawordi 6417 nnmord 6465 nnmword 6466 ac6sfi 6844 unsnfi 6864 unsnfidcel 6866 ordiso2 6980 prarloclemarch2 7340 enq0tr 7355 distrlem4prl 7505 distrlem4pru 7506 ltaprg 7540 aptiprlemu 7561 lelttr 7966 ltletr 7967 readdcan 8016 addcan 8056 addcan2 8057 ltadd2 8295 ltmul1a 8467 ltmul1 8468 divmulassap 8569 divmulasscomap 8570 lemul1a 8730 xrlelttr 9711 xrltletr 9712 xaddass 9774 xleadd1a 9778 xltadd1 9781 xlesubadd 9788 ixxdisj 9808 icoshftf1o 9896 icodisj 9897 lincmb01cmp 9908 iccf1o 9909 fztri3or 9942 ioom 10164 modqmuladdim 10270 modqmuladdnn0 10271 q2submod 10288 modqaddmulmod 10294 exp3val 10425 ltexp2a 10475 exple1 10479 expnbnd 10545 expnlbnd2 10547 expcan 10594 fiprsshashgt1 10695 maxleastb 11118 maxltsup 11122 xrltmaxsup 11158 xrmaxltsup 11159 xrmaxaddlem 11161 xrmaxadd 11162 addcn2 11211 mulcn2 11213 geoisum1c 11421 dvdsval2 11690 dvdsmodexp 11695 dvdsadd2b 11738 dvdsmod 11758 oexpneg 11772 divalglemex 11817 divalg 11819 gcdass 11903 rplpwr 11915 rppwr 11916 lcmass 11966 coprmdvds2 11974 rpmulgcd2 11976 rpdvds 11980 cncongr2 11985 rpexp 12032 znege1 12057 prmdiveq 12115 hashgcdlem 12117 odzdvds 12124 coprimeprodsq2 12137 pythagtriplem3 12146 pythagtriplem4 12147 ctinf 12201 nnminle 12220 nninfdc 12226 topssnei 12604 cnptopco 12664 cnconst2 12675 cnptoprest 12681 cnpdis 12684 upxp 12714 bldisj 12843 blgt0 12844 bl2in 12845 blss2ps 12848 blss2 12849 xblm 12859 blssps 12869 blss 12870 xmetresbl 12882 bdbl 12945 bdmopn 12946 metcnp3 12953 metcnp 12954 metcnp2 12955 dvfvalap 13092 dvcnp2cntop 13105 dvcn 13106 logdivlti 13244 |
Copyright terms: Public domain | W3C validator |