Theorem 19.23adv 1212

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 969	. 2 |- (ph -> A.xph)
2		ax-17 969	. 2 |- (ch -> A.xch)
3		19.23adv.1	. 2 |- (ph -> (ps -> ch))
4	1, 2, 3	19.23ad 1064	1 |- (ph -> (E.xps -> ch))

Syntax hints:   -> wi 3  E.wex 978

This theorem is referenced by:  ax11v2 1213  19.23advv 1295  ax11eq 1361  ax11el 1362  ax11inda 1369  sssn 2469  iununi 2611  wefrc 2938  onfr 2981  funfvop 3794  dff2 3808  elunirnALT 3860  isomin 3890  isofrlem 3892  f1oweALT 3897  undom 4424  fodomr 4469  mapen 4477  mapdom2 4480  phplem4 4497  php3 4501  pssnn 4519  ssfi 4521  domfi 4522  isfinite2 4529  fiint 4540  fodomfi 4546  fodomfib 4547  pm54.43 4552  inf3lem2 4594  zfregs 4627  r1pwcl 4667  cplem1 4700  aceq6b 4722  kmlem13 4757  zorn2lem7 4774  fodom 4778  fodomb 4780  unidom 4788  ltexpq 5060  ltbtwnpq 5064  genpnmax 5090  distrlem1pr 5107  1idpr 5113  psslinpr 5115  prlem934 5119  ltaddpr 5120  ltexprlem2 5123  ltexprlem6 5127  ltexprlem7 5128  prlem936 5135  reclem2pr 5137  reclem4pr 5139  suplem1pr 5141  recexsrlem 5192  recexsr 5196  suppsrlem 5201  suppsr2 5203  supsr 5211  suprelem 5239  axrnegex 5263  axrrecex 5264  sup2 6006  infmrcl 6024  fznt 6433  iserzext 7079  isumclim2tf 7141  isumreclt 7153  isummulc1ALT 7156  efseq0ex 7261  acdc2 7440  acdc 7445  infxpidmlem12 7514  tgval3t 7575  tgtopt 7578  basgen2t 7589  subbas2 7595  subtop 7596  metelcls 7916  iscms2lem5 7943  cmsss 7947  bcthlem31 7979  spansncv 9537  hmphsyma 10451  hmphtr 10454

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

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

Copyright terms: Public domain