Theorem r19.22dva 1736

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

Hypothesis

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

Assertion

Ref	Expression
r19.22dva	|- (ph -> (E.x e. A ps -> E.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem r19.22dva

Step	Hyp	Ref	Expression
1		r19.22dva.1	. . 3 |- ((ph /\ x e. A) -> (ps -> ch))
2	1	ex 373	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	2	r19.22dv 1734	1 |- (ph -> (E.x e. A ps -> E.x e. A ch))

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 956  E.wrex 1643

This theorem is referenced by:  dffo4 3811  noinfep 4620  cnegextlem2 5326  arch 6026  bndndx 6028  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxrunb1 6044  uzwo3lem1 6172  qbtwnxr 6225  qsqueeze 6226  fsequb2 6464  cau3ir 6860  cvg2 6867  caure 6872  cauim 6873  climcau 7100  caucvg 7107  cvgcmp3c 7130  reeff1o 7376  unbenlem 7455  infpnlem2 7458  infpn2 7460  bastop 7592  cnpco 7719  metcnp 7839  lmle 7911  iscms2lem3 7941  bcthlem21 7969  grpidinvlem3 8000  grpideu 8003  grpinveu 8014  isgrp2i 8026  ring2 8101  ubthlem5 8477  minveclem27 8515  minvecex 8522  htthlem12 8574  hhcms 9011  hhsscms 9089  projlem15 9139  projlem26 9150  projlem28 9152  nmopunt 9877  rnbra 9978  sumdmdi 10278  cdj3lem2b 10298

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-ral 1646  df-rex 1647

Copyright terms: Public domain