Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 19.21bi | Unicode version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.21bi.1 |
Ref | Expression |
---|---|
19.21bi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.21bi.1 | . 2 | |
2 | ax-4 1487 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1329 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-4 1487 |
This theorem is referenced by: 19.21bbi 1538 ax11e 1768 eqeq1 2144 eleq2 2201 r19.21bi 2518 elrab3t 2834 ssel 3086 exmidsssn 4120 copsex2t 4162 pocl 4220 ordsucim 4411 peano2 4504 funmo 5133 funun 5162 fununi 5186 imain 5200 tfrlem3-2d 6202 tfr1onlemaccex 6238 tfri1dALT 6241 tfrcllemaccex 6251 findcard 6775 findcard2 6776 findcard2s 6777 exmidpw 6795 |
Copyright terms: Public domain | W3C validator |