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 1416 | . . 3 |
3 | simpr 109 | . . . 4 | |
4 | 3 | alimi 1416 | . . 3 |
5 | 2, 4 | jca 304 | . 2 |
6 | id 19 | . . 3 | |
7 | 6 | alanimi 1420 | . 2 |
8 | 5, 7 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wal 1314 |
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 1408 ax-gen 1410 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.26-2 1443 19.26-3an 1444 albiim 1448 2albiim 1449 hband 1450 hban 1511 19.27h 1524 19.27 1525 19.28h 1526 19.28 1527 nford 1531 nfand 1532 equsexd 1692 equveli 1717 sbanv 1845 2eu4 2070 bm1.1 2102 r19.26m 2540 unss 3220 ralunb 3227 ssin 3268 intun 3772 intpr 3773 eqrelrel 4610 relop 4659 eqoprab2b 5797 dfer2 6398 |
Copyright terms: Public domain | W3C validator |