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 979

This theorem is referenced by:  funopg 3544  th3qlem1 4311  fundmen 4422  unen 4427  zorn2lem6 4780  genpss 5094  genpnnp 5095  genpcd 5096  genpnmax 5097  distrlem1pr 5114  distrlem5pr 5118  ltexprlem6 5134  reclem4pr 5146  mulgt0sr 5201  creur 6694  creui 6695  replimt 6713  pjtheu 9223  osumlem7 9574  hmeogrp 10519

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

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

Copyright terms: Public domain