Theorem 19.23adv 1584

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

Syntax hints:   -> wi 3  E.wex 1326

This theorem is referenced by:  ax11v2 1585  19.23advv 1676  ax11eq 1754  ax11el 1755  ax11inda 1762  sssn 3142  iununi 3331  iununiOLD 3332  wefrc 3652  onfr 3702  iss 4254  dffv2 4734  funfvop 4776  dff3 4790  elunirnALT 4845  isomin 4876  isofrlem 4878  f1oweALT 4883  undom 5497  ac6sfi 5509  fodomr 5547  mapen 5585  mapdom2 5588  phplem4 5605  php3 5609  pssnn 5628  ssfi 5630  domfi 5631  isfinite2 5639  fiint 5650  fodomfi 5656  fodomfib 5657  pm54.43 5662  ordiso 5683  ordtypelem7 5690  ordtype 5691  hartog 5693  inf3lem2 5720  zfregs 5754  r1pwcl 5798  cplem1 5850  aceq6b 5904  kmlem13 5939  zorn2lem7 5956  fodom 5960  fodomb 5962  unidom 5970  ltexpq 6232  ltbtwnpq 6236  genpnmax 6262  distrlem1pr 6279  1idpr 6285  psslinpr 6287  prlem934 6291  ltaddpr 6292  ltexprlem2 6295  ltexprlem6 6299  ltexprlem7 6300  prlem936 6307  reclem2pr 6309  reclem4pr 6311  suplem1pr 6313  recexsrlem 6364  recexsr 6368  suppsrlem 6373  suppsr2 6375  supsr 6383  suprelem 6411  axrnegex 6436  axrrecex 6437  sup2 7260  infmrcl 7278  fzn 7663  iserzex 8395  isumclim2f 8459  isumrecl 8471  isummulc1iALT 8474  efseq0ex 8573  acdc2 8759  acdc 8764  infxpidmlem12 8832  tgval3 8895  tgtop 8898  basgen2 8909  subbas2 8915  subtop 8916  metelcls 9243  iscms2lem5 9271  cmsss 9275  bcthlem31 9307  gapm 9462  indexfi 10174  findcard 10178  fixp 10180  fiuni 10219  uptx 10226  subtopmet 10256  fbssint 10279  fgbas 10286  elfilmap 10312  comptoppr 10332  spansncvi 11232  negn0 13655  elres 13824  fundmpss 13836  tz6.26 13913  trclss 13935  frmin 13938  wfrlem12 13968  nocvxmin 14029  hmphsyma 14882  hmphtr 14885  ioodisj 15364  elfiun 15369  finsschain 15373  ordisoOLD 15374  ordtypelem7OLD 15381  ordtypeOLD 15382  hartogOLD 15384  compsublem 15430  compsub 15431  hscptsscld 15434  alexsublem3 15439  alexsublem4 15440  alexsub 15441  conntoppr 15445  2ndcsb 15476  2ndcctbss 15478  isfne3 15482  fnessref 15503  refssfne 15504  locfincomp 15514  comppfsc 15517  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem4 15522  topjoin 15527  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  filfinnfr 15561  filssufillem 15570  uffixfr 15575  filcon 15580  fmfnfmlem1 15594  fmfnfmlem4 15597  fmfnfm 15598  sfcls 15604  fcluscomplem 15620  tailfb 15639  filnetlem3 15642  filnet 15645  findcard2 15745  indexfiOLD 15755  inficl 15757  frfi 15771  fzfi2 15787  fzn0 15789  sdc 15811  fdc 15812  txsubsp 15912  totbndss 15937  heiborlem1 15955  heiborlem32 15986  heiborlem37 15991  bfp 16009  rrntotbnd 16022  phtpcdm 16061  phtpcer 16062  riscer 16142  divrngidl 16176  erreft 16259  erdisj3 16266  prtlem17 16278  osumcllem8 17371  pexmidlem5 17382

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain