Theorem 19.23advv 1676

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

Syntax hints:   -> wi 3  E.wex 1326

This theorem is referenced by:  funopg 4454  th3qlem1 5373  fundmen 5487  unen 5493  hartog 5693  zorn2lem6 5955  genpss 6259  genpnnp 6260  genpcd 6261  genpnmax 6262  distrlem1pr 6279  distrlem5pr 6283  ltexprlem6 6299  reclem4pr 6311  mulgt0sr 6366  creur 7992  creui 7993  replim 8011  pjtheui 10868  osumlem7 11219  hmeogrp 14892  elfiun 15369  hartogOLD 15384  2ndcctbss 15478  filssufillem 15570  filnetlem3 15642  filnetlem5 15644  txmet 15925  riscer 16142

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain