Theorem reximdva 2203

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

Hypothesis

Ref	Expression
reximdva.1	|- ((ph /\ x e. A) -> (ps -> ch))

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		reximdva.1	. . 3 |- ((ph /\ x e. A) -> (ps -> ch))
2	1	ex 402	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	2	reximdvai 2201	1 |- (ph -> (E.x e. A ps -> E.x e. A ch))

Syntax hints:   -> wi 3   /\ wa 240   e. wcel 1300  E.wrex 2106

This theorem is referenced by:  dffo4 4793  noinfep 5747  cnegexlem2 6500  arch 7280  bndndx 7282  xrsupsslem 7285  xrinfmsslem 7286  xrub 7289  supxrunb1 7298  uzwo3lem1 7429  qbtwnxr 7460  qsqueeze 7461  fsequb2 7703  expnlbnd2 7903  cau3iri 8167  cvg2i 8174  caurei 8179  cauimi 8180  climcaui 8416  caucvgi 8423  cvgcmp3ci 8447  reeff1o 8691  unbenlem 8773  infpnlem2 8776  infpn2 8778  bastop1 8912  cnpnei 9043  cnpco 9046  metcnp 9165  lmle 9238  iscms2lem3 9269  bcthlem21 9297  grpidinvlem3 9330  grpideu 9333  grpinveu 9348  isgrp2i 9360  ring2 9474  ubthlem5 9876  minveclem27 9916  minvecex 9923  htthlem12 9978  exidu1 10373  hhcms 10705  hhsscms 10783  projlem15 10833  projlem26 10844  projlem28 10846  nmopun 11576  rnbra 11678  sumdmdii 11987  cdj3lem2b 12009  tz6.26 13913  frmin 13938  axfelem15 14045  nZdef 14527  ist1-2 15542  ufilen 15579  fisupg 15748  fimax2g 15769  fimaxre 15774  geomcau 15849  lmtlm 15908  totbndss 15937  bndss 15942  totbndbnd 15944  ismtybndlem 15952  heiborlem11 15965  heiborlem35 15989  heiborlem36 15990  heiborlem37 15991  rrncms 16019  prtlem15 16281  strssp1 16713  hlhght2 17038  hlrelat2 17052  ps2 17079  grpidinvlem3NEW 17111  grpideuNEW 17114  grpinveuNEW 17123

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-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain