Theorem 19.22dv 947

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

Hypothesis

Ref	Expression
19.20dv.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
19.22dv	|- (ph -> (E.xps -> E.xch))

Distinct variable group(s):   ph,x

Proof of Theorem 19.22dv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		19.20dv.1	. 2 |- (ph -> (ps -> ch))
3	1, 2	19.22d 744	1 |- (ph -> (E.xps -> E.xch))

Syntax hints:   -> wi 2  E.wex 678

This theorem is referenced by:  19.22dvv 949  immo 1043  moimv 1044  r19.22dv2 1277  ssel 1502  reupick 1578  uniss 1936  nnsuc 2389  dmss 2530  funss 2682  funssres 2698  fv3 2839  fvclss 2907  cbvfo 2923  ecelqsi 3229  mapsn 3269  ssnn 3429  unfilem1 3438  ac6s 3577  zornlem7 3609  cfub 3703  cflim 3704  nsmallpq 3877  ltexprlem1 3936  ltexprlem3 3938  ltexprlem4 3939  ltexpri 3943  prlem936 3949  reclem2pr 3951  reclem3pr 3952  suplem1pr 3955  suppsr2 4017  suppsr3 4018  supsrlem2 4020  axsup 4088  infxpidmlem10 4942  shless 5348

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-gen 677  ax-17 925

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

metamath.org