Theorem r19.20 1699

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 1646	. . 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 993	. . 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 1646	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
6		df-ral 1646	. 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 952   e. wcel 956  A.wral 1642

This theorem is referenced by:  r19.20sii 1704  tfrlem1 3902  tz7.49 3950  abianfp 3953  bnd 4703  kmlem12 4756  2climnn 7047  2climnn0 7048  climsqueeze 7084  climsqueeze2 7085  climabslem 7092  iscms2lem4 7942  osumlem4 9521

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

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

Copyright terms: Public domain