Theorem ivthlem3 7283

Description: Lemma for isupivth 7290.

Hypotheses

Ref	Expression
ivthlem3.1	|- (ph -> E.z e. RR+ A.w e. A (ps -> th))
ivthlem3.2	|- (w e. A -> (th -> ta))

Assertion

Ref	Expression
ivthlem3	|- (ph -> E.z(z e. RR+ /\ A.w e. A (ps -> ta)))

Proof of Theorem ivthlem3

Step	Hyp	Ref	Expression
1		ivthlem3.1	. 2 |- (ph -> E.z e. RR+ A.w e. A (ps -> th))
2		ivthlem3.2	. . . . . 6 |- (w e. A -> (th -> ta))
3	2	rgen 1698	. . . . 5 |- A.w e. A (th -> ta)
4		imim1 15	. . . . . 6 |- ((ps -> th) -> ((th -> ta) -> (ps -> ta)))
5	4	r19.20sii 1707	. . . . 5 |- (A.w e. A (ps -> th) -> (A.w e. A (th -> ta) -> A.w e. A (ps -> ta)))
6	3, 5	mpi 44	. . . 4 |- (A.w e. A (ps -> th) -> A.w e. A (ps -> ta))
7	6	r19.22si 1734	. . 3 |- (E.z e. RR+ A.w e. A (ps -> th) -> E.z e. RR+ A.w e. A (ps -> ta))
8		df-rex 1650	. . 3 |- (E.z e. RR+ A.w e. A (ps -> ta) <-> E.z(z e. RR+ /\ A.w e. A (ps -> ta)))
9	7, 8	sylib 198	. 2 |- (E.z e. RR+ A.w e. A (ps -> th) -> E.z(z e. RR+ /\ A.w e. A (ps -> ta)))
10	1, 9	syl 10	1 |- (ph -> E.z(z e. RR+ /\ A.w e. A (ps -> ta)))

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 958  E.wex 980  A.wral 1645  E.wrex 1646  RR+crp 5300

This theorem is referenced by:  ivthlem8 7288

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-ral 1649  df-rex 1650

Copyright terms: Public domain