Theorem 19.23advv 1297

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 groups:   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 1214	. 2 |- (ph -> (E.yps -> ch))
3	2	19.23adv 1214	1 |- (ph -> (E.xE.yps -> ch))

Syntax hints:   -> wi 3  E.wex 980

This theorem is referenced by:  funopg 3547  th3qlem1 4314  fundmen 4428  unen 4434  zorn2lem6 4793  genpss 5107  genpnnp 5108  genpcd 5109  genpnmax 5110  distrlem1pr 5127  distrlem5pr 5131  ltexprlem6 5147  reclem4pr 5159  mulgt0sr 5214  creur 6742  creui 6743  replimt 6761  pjtheu 9235  osumlem7 9584  hmeogrp 10538

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981

Copyright terms: Public domain