Theorem 19.23adv 1216

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

Hypothesis

Ref	Expression
19.23adv.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
19.23adv	⊢ (φ → (∃xψ → χ))

Distinct variable groups:   χ,x   φ,x

Proof of Theorem 19.23adv

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 ⊢ (φ → ∀xφ)
2		ax-17 973	. 2 ⊢ (χ → ∀xχ)
3		19.23adv.1	. 2 ⊢ (φ → (ψ → χ))
4	1, 2, 3	19.23ad 1068	1 ⊢ (φ → (∃xψ → χ))

Syntax hints:   → wi 3  ∃wex 982

This theorem is referenced by:  ax11v2 1217  19.23advv 1299  ax11eq 1365  ax11el 1366  ax11inda 1373  sssn 2477  iununi 2621  wefrc 2949  onfr 2992  funfvop 3809  dff2 3823  elunirnALT 3875  isomin 3905  isofrlem 3907  f1oweALT 3912  undom 4444  fodomr 4489  mapen 4497  mapdom2 4500  phplem4 4517  php3 4521  php3OLD 4522  pssnn 4544  ssfi 4547  ssfiOLD 4548  domfi 4549  domfiOLD 4550  isfinite2 4557  isfinite2OLD 4558  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  pm54.43 4581  inf3lem2 4623  zfregs 4657  r1pwcl 4697  cplem1 4730  aceq6b 4752  kmlem13 4787  zorn2lem7 4804  fodom 4808  fodomb 4810  unidom 4818  ltexpq 5092  ltbtwnpq 5096  genpnmax 5122  distrlem1pr 5139  1idpr 5145  psslinpr 5147  prlem934 5151  ltaddpr 5152  ltexprlem2 5155  ltexprlem6 5159  ltexprlem7 5160  prlem936 5167  reclem2pr 5169  reclem4pr 5171  suplem1pr 5173  recexsrlem 5224  recexsr 5228  suppsrlem 5233  suppsr2 5235  supsr 5243  suprelem 5271  axrnegex 5295  axrrecex 5296  sup2 6053  infmrcl 6071  fznt 6494  iserzext 7135  isumclim2tf 7198  isumreclt 7210  isummulc1ALT 7213  efseq0ex 7311  acdc2 7491  acdc 7496  infxpidmlem12 7564  tgval3t 7624  tgtopt 7627  basgen2t 7638  subtop 7643  metelcls 7962  iscms2lem5 7990  cmsss 7994  bcthlem31 8026  spansncv 9592  hmphsyma 10514  hmphtr 10517

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

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

Copyright terms: Public domain