![]() |
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 984 sbidm 1862 4exdistr 1928 2sb5 1995 2sb5rf 2001 sbel2x 2010 r2exf 2508 r19.41 2645 ceqsex3v 2794 ceqsrex2v 2884 rexrab 2915 rexrab2 2919 rexss 3237 inass 3360 difin2 3412 difrab 3424 reupick3 3435 inssdif0im 3505 rexdifpr 3635 rexdifsn 3739 unidif0 4185 bnd2 4191 eqvinop 4261 copsexg 4262 uniuni 4469 rabxp 4681 elvvv 4707 rexiunxp 4787 resopab2 4972 ssrnres 5089 elxp4 5134 elxp5 5135 cnvresima 5136 mptpreima 5140 coass 5165 dff1o2 5485 eqfnfv3 5636 rexsupp 5661 isoini 5840 f1oiso 5848 oprabid 5928 dfoprab2 5943 mpoeq123 5955 mpomptx 5987 resoprab2 5993 ovi3 6033 oprabex3 6154 spc2ed 6258 f1od2 6260 brtpos2 6276 mapsnen 6837 xpsnen 6847 xpcomco 6852 xpassen 6856 ltexpi 7366 enq0enq 7460 enq0tr 7463 prnmaxl 7517 prnminu 7518 genpdflem 7536 ltexprlemm 7629 suplocsrlemb 7835 axaddf 7897 axmulf 7898 rexuz 9610 rexuz2 9611 rexrp 9706 elixx3g 9931 elfz2 10045 fzdifsuc 10111 fzind2 10269 divalgb 11962 gcdass 12048 nnwosdc 12072 lcmass 12117 isprm2 12149 infpn2 12507 issubg3 13131 dfrhm2 13504 ntreq0 14092 tx1cn 14229 tx2cn 14230 blres 14394 metrest 14466 elcncf1di 14526 dedekindicclemicc 14570 |
Copyright terms: Public domain | W3C validator |