Theorem 19.23adv 1214

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

Syntax hints:   -> wi 3  E.wex 980

This theorem is referenced by:  ax11v2 1215  19.23advv 1297  ax11eq 1363  ax11el 1364  ax11inda 1371  sssn 2471  iununi 2614  wefrc 2941  onfr 2984  funfvop 3801  dff2 3815  elunirnALT 3867  isomin 3897  isofrlem 3899  f1oweALT 3904  undom 4432  fodomr 4477  mapen 4485  mapdom2 4488  phplem4 4505  php3 4509  pssnn 4527  ssfi 4529  domfi 4530  isfinite2 4537  fiint 4548  fodomfi 4554  fodomfib 4555  pm54.43 4560  inf3lem2 4602  zfregs 4635  r1pwcl 4675  cplem1 4708  aceq6b 4730  kmlem13 4765  zorn2lem7 4782  fodom 4786  fodomb 4788  unidom 4796  ltexpq 5068  ltbtwnpq 5072  genpnmax 5098  distrlem1pr 5115  1idpr 5121  psslinpr 5123  prlem934 5127  ltaddpr 5128  ltexprlem2 5131  ltexprlem6 5135  ltexprlem7 5136  prlem936 5143  reclem2pr 5145  reclem4pr 5147  suplem1pr 5149  recexsrlem 5200  recexsr 5204  suppsrlem 5209  suppsr2 5211  supsr 5219  suprelem 5247  axrnegex 5271  axrrecex 5272  sup2 6019  infmrcl 6037  fznt 6453  iserzext 7093  isumclim2tf 7156  isumreclt 7168  isummulc1ALT 7171  efseq0ex 7269  acdc2 7447  acdc 7452  infxpidmlem12 7520  tgval3t 7582  tgtopt 7585  basgen2t 7596  subbas2 7602  subtop 7603  metelcls 7922  iscms2lem5 7950  cmsss 7954  bcthlem31 7986  spansncv 9552  hmphsyma 10470  hmphtr 10473

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