MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.43 Unicode version

Theorem r19.43 3013
Description: Restricted quantifier version of 19.43 1693. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.43

Proof of Theorem r19.43
StepHypRef Expression
1 r19.35 3004 . 2
2 df-or 370 . . 3
32rexbii 2959 . 2
4 df-or 370 . . 3
5 ralnex 2903 . . . 4
65imbi1i 325 . . 3
74, 6bitr4i 252 . 2
81, 3, 73bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  A.wral 2807  E.wrex 2808
This theorem is referenced by:  r19.44v  3014  r19.45v  3015  r19.45zv  3926  r19.44zv  3927  iunun  4411  wemapsolem  7996  pythagtriplem2  14341  pythagtrip  14358  dcubic  23177  legtrid  23978  axcontlem4  24270  erdszelem11  28645  soseq  29334  seglelin  29766  diophun  30707  rexzrexnn0  30737  usgvincvad  32404  usgvincvadALT  32407  ldepslinc  33110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813
  Copyright terms: Public domain W3C validator