Theorem r19.20 1700

Description: Distribution of restricted quantification over implication.

Assertion

Ref	Expression
r19.20	|- (A.x e. A (ph -> ps) -> (A.x e. A ph -> A.x e. A ps))

Proof of Theorem r19.20

Step	Hyp	Ref	Expression
1		df-ral 1647	. . 3 |- (A.x e. A (ph -> ps) <-> A.x(x e. A -> (ph -> ps)))
2		ax-2 5	. . . 4 |- ((x e. A -> (ph -> ps)) -> ((x e. A -> ph) -> (x e. A -> ps)))
3	2	19.20ii 994	. . 3 |- (A.x(x e. A -> (ph -> ps)) -> (A.x(x e. A -> ph) -> A.x(x e. A -> ps)))
4	1, 3	sylbi 199	. 2 |- (A.x e. A (ph -> ps) -> (A.x(x e. A -> ph) -> A.x(x e. A -> ps)))
5		df-ral 1647	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
6		df-ral 1647	. 2 |- (A.x e. A ps <-> A.x(x e. A -> ps))
7	4, 5, 6	3imtr4g 552	1 |- (A.x e. A (ph -> ps) -> (A.x e. A ph -> A.x e. A ps))

Syntax hints:   -> wi 3  A.wal 953   e. wcel 957  A.wral 1643

This theorem is referenced by:  r19.20sii 1705  tfrlem1 3906  tz7.49 3954  abianfp 3957  bnd 4706  kmlem12 4759  2climnn 7055  2climnn0 7056  climsqueeze 7093  climsqueeze2 7094  climabslem 7101  iscms2lem4 7954  osumlem4 9538

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1647

Copyright terms: Public domain