Theorem ralimdv 2172

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.

Hypothesis

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

Assertion

Ref	Expression
ralimdv	|- (ph -> (A.x e. A ps -> A.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 |- (ph -> (ps -> ch))
2	1	adantr 425	. 2 |- ((ph /\ x e. A) -> (ps -> ch))
3	2	ralimdvaa 2171	1 |- (ph -> (A.x e. A ps -> A.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 1300  A.wral 2105

This theorem is referenced by:  tfindsg 3944  dffo4 4793  dffo5 4794  abianfp 5171  rankval3 5792  bndrank 5793  cfub 6056  cau3ii 8166  fsumcom 8288  fsummulc2 8294  fsumdivc 8295  fsumdivcALT 8296  fsum2mul 8297  climconsti 8354  2climnn 8362  2climnn0 8363  climaddc2 8379  climsqueeze 8400  climsqueeze2 8401  rescncf 8534  fiinbas 8885  iincld 8955  cnpco 9046  cnsscnp 9049  cncnplem4 9054  cncnp 9055  metcnss2 9177  lmuni 9229  caussi 9232  metcnp4lem2 9247  iscms2lem3 9269  lmcau 9274  nmlnoubi 9796  lnon0 9798  fipreima 10175  setlikess 13906  tz6.26 13913  frmin 13938  inpreima2 14468  inpreima5 14469  fprodadd 14713  fprodsub 14742  svli2 14826  cnrsfin 14868  neibastop3 15524  fclusfnei 15626  cocanfo 15689  fipreimaOLD 15756  heiborlem23 15977  pcohtpy 16083  unichnidl 16179  ispridl2 16186

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-ral 2109

Copyright terms: Public domain