Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > r19.42v | Unicode version |
Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
r19.42v |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.41v 2585 | . 2 | |
2 | ancom 264 | . . 3 | |
3 | 2 | rexbii 2440 | . 2 |
4 | ancom 264 | . 2 | |
5 | 1, 3, 4 | 3bitr4i 211 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wrex 2415 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-rex 2420 |
This theorem is referenced by: ceqsrexbv 2811 ceqsrex2v 2812 2reuswapdc 2883 iunrab 3855 iunin2 3871 iundif2ss 3873 iunopab 4198 elxp2 4552 cnvuni 4720 elunirn 5660 f1oiso 5720 oprabrexex2 6021 genpdflem 7308 1idprl 7391 1idpru 7392 ltexprlemm 7401 rexuz2 9369 4fvwrd4 9910 divalgb 11611 |
Copyright terms: Public domain | W3C validator |