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

Theorem bnj545 29193
 Description: Technical lemma for bnj852 29219. 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.)
Hypotheses
Ref Expression
bnj545.1
bnj545.2
bnj545.3
bnj545.4
bnj545.5
bnj545.6
bnj545.7
Assertion
Ref Expression
bnj545

Proof of Theorem bnj545
StepHypRef Expression
1 bnj545.4 . . . . . . . . . 10
21simp1bi 972 . . . . . . . . 9
3 bnj545.5 . . . . . . . . . 10
43simp1bi 972 . . . . . . . . 9
52, 4anim12i 550 . . . . . . . 8
653adant1 975 . . . . . . 7
7 bnj545.2 . . . . . . . . 9
87bnj529 29036 . . . . . . . 8
9 fndm 5536 . . . . . . . 8
10 eleq2 2496 . . . . . . . . 9
1110biimparc 474 . . . . . . . 8
128, 9, 11syl2anr 465 . . . . . . 7
136, 12syl 16 . . . . . 6
14 bnj545.6 . . . . . . 7
1514bnj930 29067 . . . . . 6
1613, 15jca 519 . . . . 5
17 bnj545.3 . . . . . 6
1817bnj931 29068 . . . . 5
1916, 18jctil 524 . . . 4
20 df-3an 938 . . . . 5
21 3anrot 941 . . . . 5
22 ancom 438 . . . . 5
2320, 21, 223bitr3i 267 . . . 4
2419, 23sylibr 204 . . 3
25 funssfv 5738 . . 3
2624, 25syl 16 . 2
271simp2bi 973 . . 3