Theorem anval 148

Description: Value of the conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Hypotheses

Ref	Expression
imval.1	|- A:*
imval.2	|- B:*

Assertion

Ref	Expression
anval	|- T. |= [[A /\ B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]

Distinct variable groups:   f,A   f,B

Proof of Theorem anval

Dummy variables p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wan 136	. . 3 |- /\ :(* -> (* -> *))
2		imval.1	. . 3 |- A:*
3		imval.2	. . 3 |- B:*
4	1, 2, 3	wov 72	. 2 |- [A /\ B]:*
5		df-an 128	. . 3 |- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
6	1, 2, 3, 5	oveq 102	. 2 |- T. |= [[A /\ B] = [A\p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]B]]
7		wv 64	. . . . . 6 |- f:(* -> (* -> *)):(* -> (* -> *))
8		wv 64	. . . . . 6 |- p:*:*
9		wv 64	. . . . . 6 |- q:*:*
10	7, 8, 9	wov 72	. . . . 5 |- [p:*f:(* -> (* -> *))q:*]:*
11	10	wl 66	. . . 4 |- \f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*]:((* -> (* -> *)) -> *)
12		wtru 43	. . . . . 6 |- T.:*
13	7, 12, 12	wov 72	. . . . 5 |- [T.f:(* -> (* -> *))T.]:*
14	13	wl 66	. . . 4 |- \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]:((* -> (* -> *)) -> *)
15	11, 14	weqi 76	. . 3 |- [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]:*
16		weq 41	. . . 4 |- = :(((* -> (* -> *)) -> *) -> (((* -> (* -> *)) -> *) -> *))
17	8, 2	weqi 76	. . . . . . 7 |- [p:* = A]:*
18	17	id 25	. . . . . 6 |- [p:* = A] |= [p:* = A]
19	7, 8, 9, 18	oveq1 99	. . . . 5 |- [p:* = A] |= [[p:*f:(* -> (* -> *))q:*] = [Af:(* -> (* -> *))q:*]]
20	10, 19	leq 91	. . . 4 |- [p:* = A] |= [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*]]
21	16, 11, 14, 20	oveq1 99	. . 3 |- [p:* = A] |= [[\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
22	7, 2, 9	wov 72	. . . . 5 |- [Af:(* -> (* -> *))q:*]:*
23	22	wl 66	. . . 4 |- \f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*]:((* -> (* -> *)) -> *)
24	9, 3	weqi 76	. . . . . . 7 |- [q:* = B]:*
25	24	id 25	. . . . . 6 |- [q:* = B] |= [q:* = B]
26	7, 2, 9, 25	oveq2 101	. . . . 5 |- [q:* = B] |= [[Af:(* -> (* -> *))q:*] = [Af:(* -> (* -> *))B]]
27	22, 26	leq 91	. . . 4 |- [q:* = B] |= [\f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [Af:(* -> (* -> *))B]]
28	16, 23, 14, 27	oveq1 99	. . 3 |- [q:* = B] |= [[\f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
29	15, 2, 3, 21, 28	ovl 117	. 2 |- T. |= [[A\p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
30	4, 6, 29	eqtri 95	1 |- T. |= [[A /\ B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]

Syntax hints:  tv 1   -> ht 2  *hb 3  \kl 6   = ke 7  T.kt 8  [kbr 9   |= 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-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:  dfan2  154