Theorem bnj979 12863

Description: First-order logic and set theory.

Hypothesis

Ref	Expression
bnj979.1	|- A.xA.y((ph /\ ps /\ x e. A /\ ch) -> th)

Assertion

Ref	Expression
bnj979	|- ((ph /\ ps) -> A.x e. A A.y(ch -> th))

Distinct variable groups:   y,A   ph,x,y   ps,x,y

Proof of Theorem bnj979

Step	Hyp	Ref	Expression
1		bnj979.1	. 2 |- A.xA.y((ph /\ ps /\ x e. A /\ ch) -> th)
2		bnj253 12092	. . . . 5 |- ((ph /\ ps /\ x e. A /\ ch) <-> ((ph /\ ps) /\ x e. A /\ ch))
3	2	imbi1i 203	. . . 4 |- (((ph /\ ps /\ x e. A /\ ch) -> th) <-> (((ph /\ ps) /\ x e. A /\ ch) -> th))
4	3	2albii 1347	. . 3 |- (A.xA.y((ph /\ ps /\ x e. A /\ ch) -> th) <-> A.xA.y(((ph /\ ps) /\ x e. A /\ ch) -> th))
5		bnj980 12862	. . . . 5 |- ((((ph /\ ps) /\ x e. A /\ ch) -> th) <-> (((ph /\ ps) /\ x e. A) -> (ch -> th)))
6		impexp 374	. . . . 5 |- ((((ph /\ ps) /\ x e. A) -> (ch -> th)) <-> ((ph /\ ps) -> (x e. A -> (ch -> th))))
7	5, 6	bitri 190	. . . 4 |- ((((ph /\ ps) /\ x e. A /\ ch) -> th) <-> ((ph /\ ps) -> (x e. A -> (ch -> th))))
8	7	2albii 1347	. . 3 |- (A.xA.y(((ph /\ ps) /\ x e. A /\ ch) -> th) <-> A.xA.y((ph /\ ps) -> (x e. A -> (ch -> th))))
9		19.21v 1663	. . . . . 6 |- (A.y((ph /\ ps) -> (x e. A -> (ch -> th))) <-> ((ph /\ ps) -> A.y(x e. A -> (ch -> th))))
10		19.21v 1663	. . . . . . 7 |- (A.y(x e. A -> (ch -> th)) <-> (x e. A -> A.y(ch -> th)))
11	10	imbi2i 202	. . . . . 6 |- (((ph /\ ps) -> A.y(x e. A -> (ch -> th))) <-> ((ph /\ ps) -> (x e. A -> A.y(ch -> th))))
12	9, 11	bitri 190	. . . . 5 |- (A.y((ph /\ ps) -> (x e. A -> (ch -> th))) <-> ((ph /\ ps) -> (x e. A -> A.y(ch -> th))))
13	12	albii 1346	. . . 4 |- (A.xA.y((ph /\ ps) -> (x e. A -> (ch -> th))) <-> A.x((ph /\ ps) -> (x e. A -> A.y(ch -> th))))
14		19.21v 1663	. . . 4 |- (A.x((ph /\ ps) -> (x e. A -> A.y(ch -> th))) <-> ((ph /\ ps) -> A.x(x e. A -> A.y(ch -> th))))
15		df-ral 2109	. . . . . 6 |- (A.x e. A A.y(ch -> th) <-> A.x(x e. A -> A.y(ch -> th)))
16	15	bicomi 189	. . . . 5 |- (A.x(x e. A -> A.y(ch -> th)) <-> A.x e. A A.y(ch -> th))
17	16	imbi2i 202	. . . 4 |- (((ph /\ ps) -> A.x(x e. A -> A.y(ch -> th))) <-> ((ph /\ ps) -> A.x e. A A.y(ch -> th)))
18	13, 14, 17	3bitri 194	. . 3 |- (A.xA.y((ph /\ ps) -> (x e. A -> (ch -> th))) <-> ((ph /\ ps) -> A.x e. A A.y(ch -> th)))
19	4, 8, 18	3bitri 194	. 2 |- (A.xA.y((ph /\ ps /\ x e. A /\ ch) -> th) <-> ((ph /\ ps) -> A.x e. A A.y(ch -> th)))
20	1, 19	mpbi 206	1 |- ((ph /\ ps) -> A.x e. A A.y(ch -> th))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858  A.wal 1296   e. wcel 1300  A.wral 2105   /\ syn-bnj17 12019

This theorem is referenced by:  bnj978 13355

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860  df-ral 2109  df-bnj17 12020

Copyright terms: Public domain