Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 19.26 | Unicode version |
Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Ref | Expression |
---|---|
19.26 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 | . . . 4 | |
2 | 1 | alimi 1442 | . . 3 |
3 | simpr 109 | . . . 4 | |
4 | 3 | alimi 1442 | . . 3 |
5 | 2, 4 | jca 304 | . 2 |
6 | id 19 | . . 3 | |
7 | 6 | alanimi 1446 | . 2 |
8 | 5, 7 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wal 1340 |
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-5 1434 ax-gen 1436 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.26-2 1469 19.26-3an 1470 albiim 1474 2albiim 1475 hband 1476 hban 1534 19.27h 1547 19.27 1548 19.28h 1549 19.28 1550 nford 1554 nfand 1555 equsexd 1716 equveli 1746 sbanv 1876 2eu4 2106 bm1.1 2149 r19.26m 2595 unss 3291 ralunb 3298 ssin 3339 intun 3849 intpr 3850 eqrelrel 4699 relop 4748 eqoprab2b 5891 dfer2 6493 omniwomnimkv 7122 |
Copyright terms: Public domain | W3C validator |