![]() |
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 999 |
. 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 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: simpll3 1038 simprl3 1044 simp1l3 1092 simp2l3 1098 simp3l3 1104 3anandirs 1348 frirrg 4349 fcofo 5782 acexmid 5871 rdgon 6384 oawordi 6467 nnmord 6515 nnmword 6516 fidifsnen 6867 dif1en 6876 ac6sfi 6895 difinfsn 7096 2omotaplemap 7253 enq0tr 7430 distrlem4prl 7580 distrlem4pru 7581 ltaprg 7615 lelttr 8042 ltletr 8043 readdcan 8093 addcan 8133 addcan2 8134 ltadd2 8372 divmulassap 8648 xrlelttr 9802 xrltletr 9803 xaddass 9865 xleadd1a 9869 xlesubadd 9879 icoshftf1o 9987 difelfzle 10129 fzo1fzo0n0 10178 modqmuladdim 10362 modqmuladdnn0 10363 modqm1p1mod0 10370 q2submod 10380 modifeq2int 10381 modqaddmulmod 10386 ltexp2a 10567 exple1 10571 expnlbnd2 10640 nn0ltexp2 10683 nn0leexp2 10684 expcan 10689 fiprsshashgt1 10790 maxleastb 11216 maxltsup 11220 xrltmaxsup 11258 xrmaxltsup 11259 xrmaxaddlem 11261 xrmaxadd 11262 addcn2 11311 mulcn2 11313 isumz 11390 dvdsmodexp 11795 modmulconst 11823 dvdsmod 11860 divalglemex 11919 divalg 11921 gcdass 12008 rplpwr 12020 rppwr 12021 nnwodc 12029 uzwodc 12030 rpmulgcd2 12087 rpdvds 12091 rpexp 12145 znege1 12170 prmdiveq 12228 hashgcdlem 12230 coprimeprodsq 12249 coprimeprodsq2 12250 pythagtriplem3 12259 pcdvdsb 12311 pcgcd1 12319 dvdsprmpweq 12326 pcbc 12341 ctinf 12423 nninfdc 12446 isnsgrp 12744 issubmnd 12775 mulgnn0p1 12926 mulgnnsubcl 12927 mulgneg 12933 mulgdirlem 12945 nmzsubg 13001 ring1eq0 13156 neiint 13516 topssnei 13533 cnptopco 13593 cnrest2 13607 cnptoprest 13610 upxp 13643 bldisj 13772 blgt0 13773 bl2in 13774 blss2ps 13777 blss2 13778 xblm 13788 blssps 13798 blss 13799 bdmopn 13875 metcnp2 13884 txmetcnp 13889 cncfmptc 13953 dvcnp2cntop 14034 dvcn 14035 logdivlti 14173 ltexp2 14231 lgsfvalg 14277 lgsneg 14296 lgsmod 14298 lgsdilem 14299 lgsdirprm 14306 lgsdir 14307 lgsdi 14309 lgsne0 14310 |
Copyright terms: Public domain | W3C validator |