Theorem reximdv 3171

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)

Hypothesis

Ref	Expression
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3166	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  r19.12  3312  r19.12OLD  3313  ss2rexv  4053  reusv3  5403  fvelima  6955  iunpw  7755  frxp  8109  ssfiALT  9171  ordtypelem2  9511  wdom2d  9572  xpwdomg  9577  cff1  10250  iunfo  10531  nqereu  10921  reclem3pr  11041  map2psrpr  11102  supsrlem  11103  1re  11211  elss2prb  14445  exprelprel  14447  o1lo1  15478  rlimcn1  15529  subcn2  15536  lo1add  15568  lo1mul  15569  pythagtriplem19  16763  vdwnnlem2  16926  ramub2  16944  sylow2alem2  19481  lsmless2x  19508  efgrelexlemb  19613  scmateALT  22006  decpmatmulsumfsupp  22267  pmatcollpw1lem1  22268  pmatcollpw2lem  22271  pm2mpmhmlem1  22312  cpmidpmatlem3  22366  cpmidgsum2  22373  tgcl  22464  neiss  22605  ssnei2  22612  tgcnp  22749  cnpco  22763  cnpresti  22784  lmcnp  22800  hausnei2  22849  1stcrest  22949  nlly2i  22972  llyss  22975  nllyss  22976  reftr  23010  lfinun  23021  txcnpi  23104  txcmplem1  23137  tx1stc  23146  nrmr0reg  23245  fbssfi  23333  fbfinnfr  23337  fgcl  23374  ufinffr  23425  elfm2  23444  fmfnfmlem1  23450  fmco  23457  fbflim2  23473  flffbas  23491  flftg  23492  cnpflf2  23496  alexsubALT  23547  cnextcn  23563  isucn2  23776  ucnima  23778  blssexps  23924  blssex  23925  mopni3  23995  neibl  24002  metss  24009  metcnp3  24041  cfilucfil  24060  metustbl  24067  psmetutop  24068  rescncf  24405  lebnum  24472  xlebnum  24473  lebnumii  24474  lmmbr  24767  fgcfil  24780  ovolsslem  24993  ovolunlem1  25006  ovoliunnul  25016  itgcn  25354  ellimc3  25388  c1lip3  25508  itgsubstlem  25557  plyss  25705  ulmclm  25891  ulmcau  25899  ulmcn  25903  rlimcxp  26468  chtppilimlem2  26967  chtppilim  26968  madess  27361  lrrecfr  27417  midex  27978  umgrnloop0  28359  usgrnloop0ALT  28452  uhgr2edg  28455  vtxduhgr0nedg  28739  wlkonl1iedg  28912  elwspths2on  29204  3cyclfrgrrn2  29530  isgrpo  29738  tpr2rico  32881  esumpcvgval  33065  omssubadd  33288  connpconn  34215  cvmliftlem15  34278  cvmlift2lem10  34292  satfdmlem  34348  fmla1  34367  satffunlem1lem2  34383  satffunlem2lem2  34386  mpomulcn  35151  fnessref  35231  fvineqsneq  36282  pibt2  36287  ptrecube  36477  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  fdc1  36603  sstotbnd3  36633  totbndss  36634  heibor1lem  36666  heibor1  36667  opidonOLD  36709  rngmgmbs4  36788  lvoli2  38441  paddss2  38678  lhpexle1lem  38867  lhpexle2lem  38869  dvhdimlem  40304  dvh3dim3N  40309  mapdh9a  40649  hdmap11lem2  40702  sn-negex12  41286  fiphp3d  41543  pell1qrss14  41592  minregex  42271  mnuop3d  43016  grumnudlem  43030  ismnushort  43046  eliuniin  43774  restuni3  43793  eliuniin2  43795  disjrnmpt2  43872  rnmptbd2lem  43939  ssfiunibd  44006  supminfxrrnmpt  44168  climrec  44306  islptre  44322  lptre2pt  44343  limsupmnfuzlem  44429  limsupre3lem  44435  limsupvaluz2  44441  supcnvlimsup  44443  liminfvalxr  44486  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  stoweidlem27  44730  stoweidlem29  44732  stoweidlem35  44738  stoweidlem48  44751  stoweidlem62  44765  fourierdlem48  44857  fourierdlem64  44873  fourierdlem65  44874  fourierdlem71  44880  fourierdlem73  44882  fourierdlem94  44903  fourierdlem103  44912  fourierdlem104  44913  fourierdlem112  44921  fourierdlem113  44922  sge0isum  45130  sge0seq  45149  meaiuninclem  45183  carageniuncllem2  45225  ovnsslelem  45263  hoidmvlelem1  45298  2reuimp  45810  afvelima  45862  sgoldbeven3prm  46438  nnsum4primes4  46444  nnsum4primesprm  46446  nnsum4primesgbe  46448  nnsum4primesle9  46450  pgrpgt2nabl  46996  opnneilv  47495  sepnsepo  47510