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 2466 | . 2 | |
2 | ancom 253 | . . 3 | |
3 | 2 | rexbii 2331 | . 2 |
4 | ancom 253 | . 2 | |
5 | 1, 3, 4 | 3bitr4i 201 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 97 wb 98 wrex 2307 |
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-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-rex 2312 |
This theorem is referenced by: ceqsrexbv 2675 ceqsrex2v 2676 2reuswapdc 2743 iunrab 3704 iunin2 3720 iundif2ss 3722 iunopab 4018 elxp2 4363 cnvuni 4521 elunirn 5405 f1oiso 5465 oprabrexex2 5757 genpdflem 6605 1idprl 6688 1idpru 6689 ltexprlemm 6698 rexuz2 8524 4fvwrd4 8997 |
Copyright terms: Public domain | W3C validator |