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 701 | . . 3 | |
2 | olc 700 | . . 3 | |
3 | 1, 2 | jaodan 786 | . 2 |
4 | orc 701 | . . . 4 | |
5 | 4 | anim2i 339 | . . 3 |
6 | olc 700 | . . . 4 | |
7 | 6 | anim2i 339 | . . 3 |
8 | 5, 7 | jaoi 705 | . 2 |
9 | 3, 8 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wo 697 |
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 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: andir 808 anddi 810 dcim 826 dcan 918 excxor 1356 sbequilem 1810 sborv 1862 r19.43 2589 indi 3323 difindiss 3330 unrab 3347 unipr 3750 uniun 3755 unopab 4007 xpundi 4595 coundir 5041 unpreima 5545 tpostpos 6161 elni2 7122 elznn0nn 9068 |
Copyright terms: Public domain | W3C validator |