Mathbox for Rodolfo Medina < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prtlem15 Structured version   Unicode version

Theorem prtlem15 30220
 Description: Lemma for prter1 30224 and prtex 30225. (Contributed by Rodolfo Medina, 13-Oct-2010.)
Assertion
Ref Expression
prtlem15
Distinct variable groups:   ,,,,,   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem prtlem15
StepHypRef Expression
1 anabs7 808 . . . . . . 7
2 an43 30193 . . . . . . . 8
32anbi2i 694 . . . . . . 7
41, 3, 23bitr4ri 278 . . . . . 6
5 prtlem14 30219 . . . . . . . 8
6 an3 30195 . . . . . . . . 9
7 elequ2 1772 . . . . . . . . . 10
87anbi2d 703 . . . . . . . . 9
96, 8syl5ibr 221 . . . . . . . 8
105, 9syl8 70 . . . . . . 7
1110imp4a 589 . . . . . 6
124, 11syl7bi 230 . . . . 5
1312expdimp 437 . . . 4
1413rexlimdv 2953 . . 3
1514reximdva 2938 . 2
16 elequ2 1772 . . . 4
17 elequ2 1772 . . . 4
1816, 17anbi12d 710 . . 3
1918cbvrexv 3089 . 2
2015, 19syl6ib 226 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wcel 1767  wrex 2815   wprt 30216 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-dif 3479  df-in 3483  df-nul 3786  df-prt 30217 This theorem is referenced by:  prter1  30224
 Copyright terms: Public domain W3C validator