Theorem 19.23advv 955

Description: Deduction from Theorem 19.23 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.23advv.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
19.23advv	|- (ph -> (E.xE.yps -> ch))

Distinct variable group(s):   ch,x   ph,x   ch,y   ph,y

Proof of Theorem 19.23advv

Step	Hyp	Ref	Expression
1		19.23advv.1	. . 3 |- (ph -> (ps -> ch))
2	1	19.23adv 954	. 2 |- (ph -> (E.yps -> ch))
3	2	19.23adv 954	1 |- (ph -> (E.xE.yps -> ch))

Syntax hints:   -> wi 2  E.wex 678

This theorem is referenced by:  th3qlem1 3250  fundmen 3333  unen 3338  zornlem6 3608  genpss 3901  genpnnp 3902  genpcd 3903  genpnmax 3904  distrlem1pr 3921  distrlem5pr 3925  ltexprlem6 3941  reclem4pr 3953  mulgt0sr 4008  axnegex 4078  creur 4532  creui 4533  replimt 4798  pjthu 5241  pjthu2 5242  osumlem7 5536

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org