Theorem anval 138

Description: Value of the conjunction.

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 126	. . 3 |- /\ :(* -> (* -> *))
2		imval.1	. . 3 |- A:*
3		imval.2	. . 3 |- B:*
4	1, 2, 3	wov 64	. 2 |- [A /\ B]:*
5		df-an 118	. . 3 |- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
6	1, 2, 3, 5	oveq 92	. 2 |- T. |= [[A /\ B] = [A\p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]B]]
7		wv 58	. . . . . 6 |- f:(* -> (* -> *)):(* -> (* -> *))
8		wv 58	. . . . . 6 |- p:*:*
9		wv 58	. . . . . 6 |- q:*:*
10	7, 8, 9	wov 64	. . . . 5 |- [p:*f:(* -> (* -> *))q:*]:*
11	10	wl 59	. . . 4 |- \f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*]:((* -> (* -> *)) -> *)
12		wtru 40	. . . . . 6 |- T.:*
13	7, 12, 12	wov 64	. . . . 5 |- [T.f:(* -> (* -> *))T.]:*
14	13	wl 59	. . . 4 |- \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]:((* -> (* -> *)) -> *)
15	11, 14	weqi 68	. . 3 |- [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]:*
16		weq 38	. . . 4 |- = :(((* -> (* -> *)) -> *) -> (((* -> (* -> *)) -> *) -> *))
17	8, 2	weqi 68	. . . . . . 7 |- [p:* = A]:*
18	17	id 25	. . . . . 6 |- [p:* = A] |= [p:* = A]
19	7, 8, 9, 18	oveq1 89	. . . . 5 |- [p:* = A] |= [[p:*f:(* -> (* -> *))q:*] = [Af:(* -> (* -> *))q:*]]
20	10, 19	leq 81	. . . 4 |- [p:* = A] |= [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*]]
21	16, 11, 14, 20	oveq1 89	. . 3 |- [p:* = A] |= [[\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
22	7, 2, 9	wov 64	. . . . 5 |- [Af:(* -> (* -> *))q:*]:*
23	22	wl 59	. . . 4 |- \f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*]:((* -> (* -> *)) -> *)
24	9, 3	weqi 68	. . . . . . 7 |- [q:* = B]:*
25	24	id 25	. . . . . 6 |- [q:* = B] |= [q:* = B]
26	7, 2, 9, 25	oveq2 91	. . . . 5 |- [q:* = B] |= [[Af:(* -> (* -> *))q:*] = [Af:(* -> (* -> *))B]]
27	22, 26	leq 81	. . . 4 |- [q:* = B] |= [\f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [Af:(* -> (* -> *))B]]
28	16, 23, 14, 27	oveq1 89	. . 3 |- [q:* = B] |= [[\f:(* -> (* -> *)) [Af:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
29	15, 2, 3, 21, 28	ovl 107	. 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 85	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 109

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-refl 39  ax-eqmp 42  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103

This theorem depends on definitions:  df-ov 65  df-an 118

This theorem is referenced by:  dfan2  144