Theorem 19.22dv 1328

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

Hypothesis

Ref	Expression
19.20dv.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
19.22dv	⊢ (φ → (∃xψ → ∃xχ))

Distinct variable group:   φ,x

Proof of Theorem 19.22dv

Step	Hyp	Ref	Expression
1		ax-17 1007	. 2 ⊢ (φ → ∀xφ)
2		19.20dv.1	. 2 ⊢ (φ → (ψ → χ))
3	1, 2	19.22d 1098	1 ⊢ (φ → (∃xψ → ∃xχ))

Syntax hints:   → wi 3  ∃wex 1016

This theorem is referenced by:  19.22dvv 1330  immo 1456  moimv 1458  r19.22dv2 1782  cgsexg 1877  cla43egv 1912  ssel 2115  reupick 2331  uniss 2588  dmss 3401  funss 3639  funssres 3657  fv3 3844  dffo4 3934  dffo5 3935  fvclss 3969  cbvfo 3999  mapsn 4486  unfilem1 4694  ac6s 4902  cfub 5058  cflim 5059  nsmallpq 5237  ltexprlem1 5296  ltexprlem3 5298  ltexprlem4 5299  ltexpri 5303  prlem936 5309  reclem2pr 5311  reclem3pr 5312  suplem1pr 5315  suppsr2 5377  suppsr3 5378  supsrlem2 5380  pre-axsup 5445  xrsupsslem 6244  xrinfmsslem 6245  supxrre 6251  ivthlem7 7492  infxpidmlem10 7773  metelcls 8176  bcthlem8 8217  bcthlem14 8223  ubthlem6 8792  cnlnssadj 10292  homcardus 11046  fiss 11419  compsub 11488  cptclsscpt 11489  reconnlem5 11511  isfne3 11543  fbssint 11626  extbas1 11641  filnet 11768  rrncms 12075

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

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

Copyright terms: Public domain