Theorem 19.23adv 954

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

Hypothesis

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

Assertion

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

Distinct variable group(s):   χ,x   φ,x

Proof of Theorem 19.23adv

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

Syntax hints:   → wi 2  ∃wex 678

This theorem is referenced by:  19.23advv 955  r19.23adv 1286  sssn 1852  iununi 2037  wefrc 2195  onfr 2237  funopfv 2886  isomin 2937  isofrlem 2939  f1oweOLD 2944  undom 3342  mapen 3386  mapdom2 3389  phplem5 3407  php3 3411  pssnn 3428  ssfi 3430  isfinite2 3437  fiint 3445  inf3lem2 3465  zfregs 3491  r1pwcl 3530  cplem1 3545  aceq6b 3565  kmlem12 3591  zornlem7 3609  fodom 3613  fodomb 3615  ltexpq 3874  ltbtwnpq 3878  genpnmax 3904  distrlem1pr 3921  1idpr 3927  psslinpr 3929  prlem934 3933  ltaddpr 3934  ltexprlem2 3937  ltexprlem6 3941  ltexprlem7 3942  prlem936 3949  reclem2pr 3951  reclem4pr 3953  suplem1pr 3955  recexsrlem 4006  recexsr 4010  suppsrlem 4015  suppsr2 4017  supsr 4025  suprelem 4053  axrecex 4079  axrnegex 4080  axrrecex 4081  sup2 4510  infxpidmlem12 4944  spansncv 5542

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org