![]() |
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: ![]() ![]() ![]() |
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 1327 rspc3ev 2810 tfisi 4509 brcogw 4716 oawordi 6373 nnmord 6421 nnmword 6422 ac6sfi 6800 unsnfi 6815 unsnfidcel 6817 ordiso2 6928 prarloclemarch2 7251 enq0tr 7266 distrlem4prl 7416 distrlem4pru 7417 ltaprg 7451 aptiprlemu 7472 lelttr 7876 ltletr 7877 readdcan 7926 addcan 7966 addcan2 7967 ltadd2 8205 ltmul1a 8377 ltmul1 8378 divmulassap 8479 divmulasscomap 8480 lemul1a 8640 xrlelttr 9619 xrltletr 9620 xaddass 9682 xleadd1a 9686 xltadd1 9689 xlesubadd 9696 ixxdisj 9716 icoshftf1o 9804 icodisj 9805 lincmb01cmp 9816 iccf1o 9817 fztri3or 9850 ioom 10069 modqmuladdim 10171 modqmuladdnn0 10172 q2submod 10189 modqaddmulmod 10195 exp3val 10326 ltexp2a 10376 exple1 10380 expnbnd 10446 expnlbnd2 10448 expcan 10494 fiprsshashgt1 10595 maxleastb 11018 maxltsup 11022 xrltmaxsup 11058 xrmaxltsup 11059 xrmaxaddlem 11061 xrmaxadd 11062 addcn2 11111 mulcn2 11113 geoisum1c 11321 dvdsval2 11532 dvdsadd2b 11576 dvdsmod 11596 oexpneg 11610 divalglemex 11655 divalg 11657 gcdass 11739 rplpwr 11751 rppwr 11752 lcmass 11802 coprmdvds2 11810 rpmulgcd2 11812 rpdvds 11816 cncongr2 11821 rpexp 11867 znege1 11892 hashgcdlem 11939 ctinf 11979 topssnei 12370 cnptopco 12430 cnconst2 12441 cnptoprest 12447 cnpdis 12450 upxp 12480 bldisj 12609 blgt0 12610 bl2in 12611 blss2ps 12614 blss2 12615 xblm 12625 blssps 12635 blss 12636 xmetresbl 12648 bdbl 12711 bdmopn 12712 metcnp3 12719 metcnp 12720 metcnp2 12721 dvfvalap 12858 dvcnp2cntop 12871 dvcn 12872 logdivlti 13010 |
Copyright terms: Public domain | W3C validator |