Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > andi | Unicode version |
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
Ref | Expression |
---|---|
andi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orc 707 | . . 3 | |
2 | olc 706 | . . 3 | |
3 | 1, 2 | jaodan 792 | . 2 |
4 | orc 707 | . . . 4 | |
5 | 4 | anim2i 340 | . . 3 |
6 | olc 706 | . . . 4 | |
7 | 6 | anim2i 340 | . . 3 |
8 | 5, 7 | jaoi 711 | . 2 |
9 | 3, 8 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wo 703 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: andir 814 anddi 816 dcim 836 dcan 928 excxor 1373 sbequilem 1831 sborv 1883 r19.43 2628 indi 3374 difindiss 3381 unrab 3398 unipr 3810 uniun 3815 unopab 4068 xpundi 4667 coundir 5113 unpreima 5621 tpostpos 6243 elni2 7276 elznn0nn 9226 |
Copyright terms: Public domain | W3C validator |