![]() |
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 395 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | anasss 394 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | impbii 125 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpan10 463 an12 533 an32 534 an13 535 an31 536 an4 558 3anass 949 sbidm 1805 4exdistr 1868 2sb5 1934 2sb5rf 1940 sbel2x 1949 r2exf 2427 r19.41 2560 ceqsex3v 2699 ceqsrex2v 2787 rexrab 2816 rexrab2 2820 rexss 3130 inass 3252 difin2 3304 difrab 3316 reupick3 3327 inssdif0im 3396 rexdifsn 3621 unidif0 4051 bnd2 4057 eqvinop 4125 copsexg 4126 uniuni 4332 rabxp 4536 elvvv 4562 rexiunxp 4641 resopab2 4824 ssrnres 4939 elxp4 4984 elxp5 4985 cnvresima 4986 mptpreima 4990 coass 5015 dff1o2 5328 eqfnfv3 5474 rexsupp 5498 isoini 5673 f1oiso 5681 oprabid 5757 dfoprab2 5772 mpoeq123 5784 mpomptx 5816 resoprab2 5822 ovi3 5861 oprabex3 5981 spc2ed 6084 f1od2 6086 brtpos2 6102 mapsnen 6659 xpsnen 6668 xpcomco 6673 xpassen 6677 ltexpi 7090 enq0enq 7184 enq0tr 7187 prnmaxl 7241 prnminu 7242 genpdflem 7260 ltexprlemm 7353 axaddf 7600 axmulf 7601 rexuz 9274 rexuz2 9275 rexrp 9362 elixx3g 9574 elfz2 9687 fzdifsuc 9751 fzind2 9906 divalgb 11467 gcdass 11546 lcmass 11609 isprm2 11641 ntreq0 12141 tx1cn 12277 tx2cn 12278 blres 12420 metrest 12492 elcncf1di 12549 |
Copyright terms: Public domain | W3C validator |