Theorem 19.23adv 1251

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

Syntax hints:   -> wi 3  E.wex 1016

This theorem is referenced by:  ax11v2 1252  19.23advv 1335  ax11eq 1402  ax11el 1403  ax11inda 1410  sssn 2538  iununi 2686  wefrc 2970  onfr 3014  funfvop 3917  dff3 3931  elunirnALT 3983  isomin 4013  isofrlem 4015  f1oweALT 4020  undom 4579  ac6sfi 4591  fodomr 4628  mapen 4638  mapdom2 4641  phplem4 4658  php3 4662  pssnn 4681  ssfi 4683  domfi 4684  isfinite2 4692  fiint 4703  fodomfi 4709  fodomfib 4710  pm54.43 4715  inf3lem2 4759  zfregs 4793  r1pwcl 4833  cplem1 4866  aceq6b 4888  kmlem13 4923  zorn2lem7 4940  fodom 4944  fodomb 4946  unidom 4954  ltexpq 5234  ltbtwnpq 5238  genpnmax 5264  distrlem1pr 5281  1idpr 5287  psslinpr 5289  prlem934 5293  ltaddpr 5294  ltexprlem2 5297  ltexprlem6 5301  ltexprlem7 5302  prlem936 5309  reclem2pr 5311  reclem4pr 5313  suplem1pr 5315  recexsrlem 5366  recexsr 5370  suppsrlem 5375  suppsr2 5377  supsr 5385  suprelem 5413  axrnegex 5437  axrrecex 5438  sup2 6219  infmrcl 6237  fzn 6621  iserzex 7338  isumclim2f 7402  isumrecl 7414  isummulc1iALT 7417  efseq0ex 7516  acdc2 7702  acdc 7707  infxpidmlem12 7775  tgval3 7837  tgtop 7840  basgen2 7851  subbas2 7857  subtop 7858  metelcls 8176  iscms2lem5 8204  cmsss 8208  bcthlem31 8240  spansncvi 9875  hmphsyma 11034  hmphtr 11037  ioodisj 11413  fiuni 11420  elfiun 11421  finsschain 11425  ordiso 11426  ordtypelem7 11433  ordtype 11434  hartog 11436  compsublem 11487  compsub 11488  hscptsscld 11491  comptoppr 11495  alexsublem3 11498  alexsublem4 11499  alexsub 11500  conntoppr 11504  subtopmet 11506  2ndcsb 11537  2ndcctbss 11539  isfne3 11543  fnessref 11564  refssfne 11565  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem4 11583  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  fbssint 11626  fgbas 11636  filfinnfr 11646  filssufillem 11655  uffixfr 11660  filcon 11665  elfilmap 11690  fmfnfmlem1 11700  fmfnfmlem4 11703  fmfnfm 11704  sfcls 11716  fcluscomplem 11732  tailfb 11762  filnetlem3 11765  filnet 11768  gapm 11784  fixp 11840  indexf 11847  inficl 11849  sdc 11877  metsstop 11909  uptx 11978  txsubsp 11983  totbndss 11993  heiborlem1 12011  heiborlem32 12042  heiborlem37 12047  bfp 12065  rrntotbnd 12078  phtpcdm 12103  phtpcer 12104

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017

Copyright terms: Public domain