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 633 | . . 3 | |
2 | olc 632 | . . 3 | |
3 | 1, 2 | jaodan 710 | . 2 |
4 | orc 633 | . . . 4 | |
5 | 4 | anim2i 324 | . . 3 |
6 | olc 632 | . . . 4 | |
7 | 6 | anim2i 324 | . . 3 |
8 | 5, 7 | jaoi 636 | . 2 |
9 | 3, 8 | impbii 117 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 97 wb 98 wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: andir 732 anddi 734 dcim 784 dcan 842 excxor 1269 sbequilem 1719 sborv 1770 r19.43 2468 indi 3184 difindiss 3191 unrab 3208 unipr 3594 uniun 3599 unopab 3836 xpundi 4396 coundir 4823 unpreima 5292 tpostpos 5879 elni2 6412 elznn0nn 8259 |
Copyright terms: Public domain | W3C validator |