Theorem 19.23adv 1256

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

Hypothesis

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

Assertion

Ref	Expression
19.23adv	|- (ph -> (E.xps -> ch))

Distinct variable groups:   ch,x   ph,x

Proof of Theorem 19.23adv

Step	Hyp	Ref	Expression
1		ax-17 1012	. 2 |- (ph -> A.xph)
2		ax-17 1012	. 2 |- (ch -> A.xch)
3		19.23adv.1	. 2 |- (ph -> (ps -> ch))
4	1, 2, 3	19.23ad 1107	1 |- (ph -> (E.xps -> ch))

Syntax hints:   -> wi 3  E.wex 1021

This theorem is referenced by:  ax11v2 1257  19.23advv 1339  ax11eq 1405  ax11el 1406  ax11inda 1413  sssn 2527  iununi 2671  wefrc 3000  onfr 3043  funfvop 3860  dff2 3874  elunirnALT 3926  isomin 3957  isofrlem 3959  f1oweALT 3964  undom 4501  fodomr 4546  mapen 4556  mapdom2 4559  phplem4 4576  php3 4580  pssnn 4599  ssfi 4601  domfi 4602  isfinite2 4609  fiint 4620  fodomfi 4626  fodomfib 4627  pm54.43 4632  inf3lem2 4676  zfregs 4709  r1pwcl 4749  cplem1 4782  aceq6b 4804  kmlem13 4839  zorn2lem7 4856  fodom 4860  fodomb 4862  unidom 4870  ltexpq 5145  ltbtwnpq 5149  genpnmax 5175  distrlem1pr 5192  1idpr 5198  psslinpr 5200  prlem934 5204  ltaddpr 5205  ltexprlem2 5208  ltexprlem6 5212  ltexprlem7 5213  prlem936 5220  reclem2pr 5222  reclem4pr 5224  suplem1pr 5226  recexsrlem 5277  recexsr 5281  suppsrlem 5286  suppsr2 5288  supsr 5296  suprelem 5324  axrnegex 5348  axrrecex 5349  sup2 6133  infmrcl 6151  fzn 6519  iserzex 7225  isumclim2f 7288  isumrecl 7300  isummulc1iALT 7303  efseq0ex 7401  acdc2 7582  acdc 7587  infxpidmlem12 7655  tgval3 7714  tgtop 7717  basgen2 7728  subtop 7733  metelcls 8050  iscms2lem5 8078  cmsss 8082  bcthlem31 8114  spansncvi 9680  hmphsyma 10622  hmphtr 10625

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022

Copyright terms: Public domain