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

Theorem constr3lem1 23710
 Description: Lemma for constr3trl 23724 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.)
Hypotheses
Ref Expression
constr3cycl.f
constr3cycl.p
Assertion
Ref Expression
constr3lem1

Proof of Theorem constr3lem1
StepHypRef Expression
1 constr3cycl.f . . 3
2 tpex 6492 . . 3
31, 2eqeltri 2538 . 2
4 constr3cycl.p . . 3
5 prex 4645 . . . 4
6 prex 4645 . . . 4
75, 6unex 6491 . . 3
84, 7eqeltri 2538 . 2
93, 8pm3.2i 455 1
 Colors of variables: wff setvar class Syntax hints:   wa 369   wceq 1370   wcel 1758  cvv 3078   cun 3437  cpr 3990  ctp 3992  cop 3994  ccnv 4950  cfv 5529  cc0 9397  c1 9398  c2 10486  c3 10487 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642  ax-un 6485 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rex 2805  df-v 3080  df-dif 3442  df-un 3444  df-nul 3749  df-sn 3989  df-pr 3991  df-tp 3993  df-uni 4203 This theorem is referenced by:  constr3trl  23724  constr3pth  23725  constr3cycl  23726
 Copyright terms: Public domain W3C validator