Theorem reximdv 3168

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 3163	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2104  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  r19.12  3309  r19.12OLD  3310  ss2rexv  4052  reusv3  5402  fvelima  6956  iunpw  7760  frxp  8114  ssfiALT  9176  ordtypelem2  9516  wdom2d  9577  xpwdomg  9582  cff1  10255  iunfo  10536  nqereu  10926  reclem3pr  11046  map2psrpr  11107  supsrlem  11108  1re  11218  elss2prb  14452  exprelprel  14454  o1lo1  15485  rlimcn1  15536  subcn2  15543  lo1add  15575  lo1mul  15576  pythagtriplem19  16770  vdwnnlem2  16933  ramub2  16951  sylow2alem2  19527  lsmless2x  19554  efgrelexlemb  19659  scmateALT  22234  decpmatmulsumfsupp  22495  pmatcollpw1lem1  22496  pmatcollpw2lem  22499  pm2mpmhmlem1  22540  cpmidpmatlem3  22594  cpmidgsum2  22601  tgcl  22692  neiss  22833  ssnei2  22840  tgcnp  22977  cnpco  22991  cnpresti  23012  lmcnp  23028  hausnei2  23077  1stcrest  23177  nlly2i  23200  llyss  23203  nllyss  23204  reftr  23238  lfinun  23249  txcnpi  23332  txcmplem1  23365  tx1stc  23374  nrmr0reg  23473  fbssfi  23561  fbfinnfr  23565  fgcl  23602  ufinffr  23653  elfm2  23672  fmfnfmlem1  23678  fmco  23685  fbflim2  23701  flffbas  23719  flftg  23720  cnpflf2  23724  alexsubALT  23775  cnextcn  23791  isucn2  24004  ucnima  24006  blssexps  24152  blssex  24153  mopni3  24223  neibl  24230  metss  24237  metcnp3  24269  cfilucfil  24288  metustbl  24295  psmetutop  24296  mpomulcn  24605  rescncf  24637  lebnum  24710  xlebnum  24711  lebnumii  24712  lmmbr  25006  fgcfil  25019  ovolsslem  25233  ovolunlem1  25246  ovoliunnul  25256  itgcn  25594  ellimc3  25628  c1lip3  25751  itgsubstlem  25800  plyss  25948  ulmclm  26135  ulmcau  26143  ulmcn  26147  rlimcxp  26714  chtppilimlem2  27213  chtppilim  27214  madess  27608  lrrecfr  27665  midex  28255  umgrnloop0  28636  usgrnloop0ALT  28729  uhgr2edg  28732  vtxduhgr0nedg  29016  wlkonl1iedg  29189  elwspths2on  29481  3cyclfrgrrn2  29807  isgrpo  30017  tpr2rico  33190  esumpcvgval  33374  omssubadd  33597  connpconn  34524  cvmliftlem15  34587  cvmlift2lem10  34601  satfdmlem  34657  fmla1  34676  satffunlem1lem2  34692  satffunlem2lem2  34695  fnessref  35545  fvineqsneq  36596  pibt2  36601  ptrecube  36791  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  fdc1  36917  sstotbnd3  36947  totbndss  36948  heibor1lem  36980  heibor1  36981  opidonOLD  37023  rngmgmbs4  37102  lvoli2  38755  paddss2  38992  lhpexle1lem  39181  lhpexle2lem  39183  dvhdimlem  40618  dvh3dim3N  40623  mapdh9a  40963  hdmap11lem2  41016  sn-negex12  41591  fiphp3d  41859  pell1qrss14  41908  minregex  42587  mnuop3d  43332  grumnudlem  43346  ismnushort  43362  eliuniin  44089  restuni3  44108  eliuniin2  44110  disjrnmpt2  44185  rnmptbd2lem  44250  ssfiunibd  44317  supminfxrrnmpt  44479  climrec  44617  islptre  44633  lptre2pt  44654  limsupmnfuzlem  44740  limsupre3lem  44746  limsupvaluz2  44752  supcnvlimsup  44754  liminfvalxr  44797  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  stoweidlem27  45041  stoweidlem29  45043  stoweidlem35  45049  stoweidlem48  45062  stoweidlem62  45076  fourierdlem48  45168  fourierdlem64  45184  fourierdlem65  45185  fourierdlem71  45191  fourierdlem73  45193  fourierdlem94  45214  fourierdlem103  45223  fourierdlem104  45224  fourierdlem112  45232  fourierdlem113  45233  sge0isum  45441  sge0seq  45460  meaiuninclem  45494  carageniuncllem2  45536  ovnsslelem  45574  hoidmvlelem1  45609  2reuimp  46121  afvelima  46173  sgoldbeven3prm  46749  nnsum4primes4  46755  nnsum4primesprm  46757  nnsum4primesgbe  46759  nnsum4primesle9  46761  pgrpgt2nabl  47130  opnneilv  47628  sepnsepo  47643