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 702 | . . 3 | |
2 | olc 701 | . . 3 | |
3 | 1, 2 | jaodan 787 | . 2 |
4 | orc 702 | . . . 4 | |
5 | 4 | anim2i 340 | . . 3 |
6 | olc 701 | . . . 4 | |
7 | 6 | anim2i 340 | . . 3 |
8 | 5, 7 | jaoi 706 | . 2 |
9 | 3, 8 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wo 698 |
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 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: andir 809 anddi 811 dcim 827 dcan 919 excxor 1360 sbequilem 1818 sborv 1870 r19.43 2615 indi 3354 difindiss 3361 unrab 3378 unipr 3786 uniun 3791 unopab 4043 xpundi 4642 coundir 5088 unpreima 5592 tpostpos 6211 elni2 7234 elznn0nn 9181 |
Copyright terms: Public domain | W3C validator |