Theorem r19.20 1694

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 1641	. . 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 992	. . 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 1641	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
6		df-ral 1641	. 2 |- (A.x e. A ps <-> A.x(x e. A -> ps))
7	4, 5, 6	3imtr4g 551	1 |- (A.x e. A (ph -> ps) -> (A.x e. A ph -> A.x e. A ps))

Syntax hints:   -> wi 3  A.wal 951   e. wcel 955  A.wral 1637

This theorem is referenced by:  r19.20sii 1699  tfrlem1 3896  tz7.49 3944  abianfp 3947  bnd 4695  kmlem12 4748  2climnn 7039  2climnn0 7040  climsqueeze 7076  climsqueeze2 7077  climabslem 7084  iscms2lem4 7926  osumlem4 9498

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

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

Copyright terms: Public domain