Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  a12study10 Unicode version

Theorem a12study10 29758
 Description: Experiment to study ax12o 1887. (Contributed by NM, 16-Dec-1015.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
a12study10
Distinct variable groups:   ,   ,

Proof of Theorem a12study10
StepHypRef Expression
1 ax9v 1645 . . 3
2 df-ex 1532 . . 3
31, 2mpbir 200 . 2
4 hbe1 1717 . . . 4
5 hba1 1731 . . . 4
64, 5hbim 1737 . . 3
7 ax-17 1606 . . . . . . . 8
8 ax-11 1727 . . . . . . . 8
97, 8syl5 28 . . . . . . 7
10 equequ1 1667 . . . . . . . . . . . 12
1110notbid 285 . . . . . . . . . . 11
1211pm5.74i 236 . . . . . . . . . 10
13 imnan 411 . . . . . . . . . 10
1412, 13bitri 240 . . . . . . . . 9
1514albii 1556 . . . . . . . 8
16 alnex 1533 . . . . . . . 8
1715, 16bitri 240 . . . . . . 7
189, 17syl6ib 217 . . . . . 6
1918con4d 97 . . . . 5
20 ax-17 1606 . . . . 5
2119, 20syl6 29 . . . 4
22 ax-11 1727 . . . . 5
23 ax-8 1661 . . . . . . 7
2423a2i 12 . . . . . 6
2524alimi 1549 . . . . 5
2622, 25syl6 29 . . . 4
2721, 26syld 40 . . 3
286, 27exlimih 1741 . 2
293, 28ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 358  wal 1530  wex 1531 This theorem is referenced by:  a12study11  29760 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
 Copyright terms: Public domain W3C validator