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

Theorem bnj1186 29377
 Description: Technical lemma for bnj69 29380. 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 1914 . . . . . . 7
32exbii 1593 . . . . . 6
41, 3mpbi 201 . . . . 5
5419.37aiv 1924 . . . 4
6 19.28v 1919 . . . . 5
76exbii 1593 . . . 4
85, 7sylib 190 . . 3
9 df-ral 2711 . . . . 5
109anbi2i 677 . . . 4
1110exbii 1593 . . 3
128, 11sylibr 205 . 2
13 df-rex 2712 . 2
1412, 13sylibr 205 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 360  wal 1550  wex 1551   wcel 1726  wral 2706  wrex 2707   class class class wbr 4213 This theorem is referenced by:  bnj1190  29378 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2711  df-rex 2712
 Copyright terms: Public domain W3C validator