Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  r19.42v Unicode version

Theorem r19.42v 2512
 Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
Assertion
Ref Expression
r19.42v
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem r19.42v
StepHypRef Expression
1 r19.41v 2511 . 2
2 ancom 262 . . 3
32rexbii 2374 . 2
4 ancom 262 . 2
51, 3, 43bitr4i 210 1
 Colors of variables: wff set class Syntax hints:   wa 102   wb 103  wrex 2350 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468 This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-rex 2355 This theorem is referenced by:  ceqsrexbv  2727  ceqsrex2v  2728  2reuswapdc  2795  iunrab  3733  iunin2  3749  iundif2ss  3751  iunopab  4044  elxp2  4389  cnvuni  4549  elunirn  5437  f1oiso  5496  oprabrexex2  5788  genpdflem  6759  1idprl  6842  1idpru  6843  ltexprlemm  6852  rexuz2  8750  4fvwrd4  9227  divalgb  10469
 Copyright terms: Public domain W3C validator