![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anass | Unicode version |
Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
anass |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anassrs 400 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | anasss 399 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | impbii 126 |
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 |
This theorem is referenced by: bianass 469 mpan10 474 an12 561 an32 562 an13 563 an31 564 an4 586 3anass 982 sbidm 1851 4exdistr 1916 2sb5 1983 2sb5rf 1989 sbel2x 1998 r2exf 2495 r19.41 2632 ceqsex3v 2779 ceqsrex2v 2869 rexrab 2900 rexrab2 2904 rexss 3222 inass 3345 difin2 3397 difrab 3409 reupick3 3420 inssdif0im 3490 rexdifpr 3620 rexdifsn 3724 unidif0 4167 bnd2 4173 eqvinop 4243 copsexg 4244 uniuni 4451 rabxp 4663 elvvv 4689 rexiunxp 4769 resopab2 4954 ssrnres 5071 elxp4 5116 elxp5 5117 cnvresima 5118 mptpreima 5122 coass 5147 dff1o2 5466 eqfnfv3 5615 rexsupp 5640 isoini 5818 f1oiso 5826 oprabid 5906 dfoprab2 5921 mpoeq123 5933 mpomptx 5965 resoprab2 5971 ovi3 6010 oprabex3 6129 spc2ed 6233 f1od2 6235 brtpos2 6251 mapsnen 6810 xpsnen 6820 xpcomco 6825 xpassen 6829 ltexpi 7335 enq0enq 7429 enq0tr 7432 prnmaxl 7486 prnminu 7487 genpdflem 7505 ltexprlemm 7598 suplocsrlemb 7804 axaddf 7866 axmulf 7867 rexuz 9578 rexuz2 9579 rexrp 9674 elixx3g 9899 elfz2 10013 fzdifsuc 10078 fzind2 10236 divalgb 11924 gcdass 12010 nnwosdc 12034 lcmass 12079 isprm2 12111 infpn2 12451 issubg3 13045 ntreq0 13563 tx1cn 13700 tx2cn 13701 blres 13865 metrest 13937 elcncf1di 13997 dedekindicclemicc 14041 |
Copyright terms: Public domain | W3C validator |