Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  dfan2 Unicode version

Theorem dfan2 154
 Description: An alternative definition of the "and" term in terms of the context conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)
Hypotheses
Ref Expression
dfan2.1
dfan2.2
Assertion
Ref Expression
dfan2

Proof of Theorem dfan2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wan 136 . . . . . 6
2 dfan2.1 . . . . . 6
3 dfan2.2 . . . . . 6
41, 2, 3wov 72 . . . . 5
54trud 27 . . . 4
6 wv 64 . . . . . . . 8
76, 2, 3wov 72 . . . . . . 7
87wl 66 . . . . . 6
9 wv 64 . . . . . . . 8
109wl 66 . . . . . . 7
1110wl 66 . . . . . 6
128, 11wc 50 . . . . 5
134id 25 . . . . . . 7
142, 3anval 148 . . . . . . . 8
154, 14a1i 28 . . . . . . 7
1613, 15mpbi 82 . . . . . 6
178, 11, 16ceq1 89 . . . . 5
186, 11weqi 76 . . . . . . . . . 10
1918id 25 . . . . . . . . 9
206, 2, 3, 19oveq 102 . . . . . . . 8
219, 2weqi 76 . . . . . . . . . . 11
2221id 25 . . . . . . . . . 10
23 wv 64 . . . . . . . . . . . 12
2423, 3weqi 76 . . . . . . . . . . 11
2524, 2eqid 83 . . . . . . . . . 10
269, 2, 3, 22, 25ovl 117 . . . . . . . . 9
2718, 26a1i 28 . . . . . . . 8
287, 20, 27eqtri 95 . . . . . . 7
297, 11, 28cl 116 . . . . . 6
304, 29a1i 28 . . . . 5
31 wtru 43 . . . . . . . 8
326, 31, 31wov 72 . . . . . . 7
336, 31, 31, 19oveq 102 . . . . . . . 8
349, 31weqi 76 . . . . . . . . . . 11
3534id 25 . . . . . . . . . 10
3623, 31weqi 76 . . . . . . . . . . 11
3736, 31eqid 83 . . . . . . . . . 10
389, 31, 31, 35, 37ovl 117 . . . . . . . . 9
3918, 38a1i 28 . . . . . . . 8
4032, 33, 39eqtri 95 . . . . . . 7
4132, 11, 40cl 116 . . . . . 6
424, 41a1i 28 . . . . 5
4312, 17, 30, 423eqtr3i 97 . . . 4
445, 43mpbir 87 . . 3
4523wl 66 . . . . . . 7
4645wl 66 . . . . . 6
478, 46wc 50 . . . . 5
488, 46, 16ceq1 89 . . . . 5
496, 46weqi 76 . . . . . . . . . 10
5049id 25 . . . . . . . . 9
516, 2, 3, 50oveq 102 . . . . . . . 8
527, 46, 51cl 116 . . . . . . 7
5321, 23eqid 83 . . . . . . . . 9
5424id 25 . . . . . . . . 9
5523, 2, 3, 53, 54ovl 117 . . . . . . . 8
5631, 55a1i 28 . . . . . . 7
5747, 52, 56eqtri 95 . . . . . 6
584, 57a1i 28 . . . . 5
596, 31, 31, 50oveq 102 . . . . . . . 8
6034, 23eqid 83 . . . . . . . . . 10
6136id 25 . . . . . . . . . 10
6223, 31, 31, 60, 61ovl 117 . . . . . . . . 9
6349, 62a1i 28 . . . . . . . 8
6432, 59, 63eqtri 95 . . . . . . 7
6532, 46, 64cl 116 . . . . . 6
664, 65a1i 28 . . . . 5
6747, 48, 58, 663eqtr3i 97 . . . 4
685, 67mpbir 87 . . 3
6944, 68jca 18 . 2
702, 3simpl 22 . . . . . . 7
7170eqtru 86 . . . . . 6
722, 3simpr 23 . . . . . . 7
7372eqtru 86 . . . . . 6
746, 31, 31, 71, 73oveq12 100 . . . . 5
7532, 74eqcomi 79 . . . 4
767, 75leq 91 . . 3
7770ax-cb1 29 . . . 4
7877, 14a1i 28 . . 3
7976, 78mpbir 87 . 2
8069, 79dedi 85 1
 Colors of variables: type var term Syntax hints:  tv 1   ht 2  hb 3  kc 5  kl 6   ke 7  kt 8  kbr 9  kct 10   wffMMJ2 11  wffMMJ2t 12   tan 119 This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-wctl 31  ax-wctr 32  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wct 47  ax-wc 49  ax-ceq 51  ax-wv 63  ax-wl 65  ax-beta 67  ax-distrc 68  ax-leq 69  ax-distrl 70  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80  ax-hbl1 103  ax-17 105  ax-inst 113 This theorem depends on definitions:  df-ov 73  df-an 128 This theorem is referenced by:  hbct  155  mpd  156  ex  158
 Copyright terms: Public domain W3C validator