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

Theorem bnj545 29699
 Description: Technical lemma for bnj852 29725. 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 1022 . . . . . . . . 9
3 bnj545.5 . . . . . . . . . 10
43simp1bi 1022 . . . . . . . . 9
52, 4anim12i 569 . . . . . . . 8
653adant1 1025 . . . . . . 7
7 bnj545.2 . . . . . . . . 9
87bnj529 29544 . . . . . . . 8
9 fndm 5673 . . . . . . . 8
10 eleq2 2517 . . . . . . . . 9
1110biimparc 490 . . . . . . . 8
128, 9, 11syl2anr 481 . . . . . . 7
136, 12syl 17 . . . . . 6
14 bnj545.6 . . . . . . 7
1514bnj930 29574 . . . . . 6
1613, 15jca 535 . . . . 5
17 bnj545.3 . . . . . 6
1817bnj931 29575 . . . . 5
1916, 18jctil 540 . . . 4
20 df-3an 986 . . . . 5
21 3anrot 989 . . . . 5
22 ancom 452 . . . . 5
2320, 21, 223bitr3i 279 . . . 4
2419, 23sylibr 216 . . 3
25 funssfv 5878 . . 3
2624, 25syl 17 . 2
271simp2bi 1023 . . 3