Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1186 Structured version   Unicode version

Theorem bnj1186 32280
 Description: Technical lemma for bnj69 32283. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypothesis
Ref Expression
bnj1186.1
Assertion
Ref Expression
bnj1186
Distinct variable groups:   ,   ,,   ,,
Allowed substitution hints:   ()   (,)

Proof of Theorem bnj1186
StepHypRef Expression
1 bnj1186.1 . . . . . 6
2 19.21v 1910 . . . . . . 7
32exbii 1635 . . . . . 6
41, 3mpbi 208 . . . . 5
5419.37aiv 1920 . . . 4
6 19.28v 1915 . . . . 5
76exbii 1635 . . . 4
85, 7sylib 196 . . 3
9 df-ral 2797 . . . . 5
109anbi2i 694 . . . 4
1110exbii 1635 . . 3
128, 11sylibr 212 . 2
13 df-rex 2798 . 2
1412, 13sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 369  wal 1368  wex 1587   wcel 1757  wral 2792  wrex 2793   class class class wbr 4376 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 1709  ax-7 1729  ax-10 1776  ax-12 1793 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2797  df-rex 2798 This theorem is referenced by:  bnj1190  32281
 Copyright terms: Public domain W3C validator