Theorem reximdv 3153

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.12  3287  ss2rexv  4007  reusv3  5352  fvelima  6907  iunpw  7726  frxp  8078  nnaordex2  8577  ssfiALT  9110  ordtypelem2  9436  wdom2d  9497  xpwdomg  9502  cff1  10180  iunfo  10461  nqereu  10852  reclem3pr  10972  map2psrpr  11033  supsrlem  11034  1re  11144  elss2prb  14423  exprelprel  14425  o1lo1  15472  rlimcn1  15523  subcn2  15530  lo1add  15562  lo1mul  15563  pythagtriplem19  16773  vdwnnlem2  16936  ramub2  16954  sylow2alem2  19559  lsmless2x  19586  efgrelexlemb  19691  scmateALT  22468  decpmatmulsumfsupp  22729  pmatcollpw1lem1  22730  pmatcollpw2lem  22733  pm2mpmhmlem1  22774  cpmidpmatlem3  22828  cpmidgsum2  22835  tgcl  22925  neiss  23065  ssnei2  23072  tgcnp  23209  cnpco  23223  cnpresti  23244  lmcnp  23260  hausnei2  23309  1stcrest  23409  nlly2i  23432  llyss  23435  nllyss  23436  reftr  23470  lfinun  23481  txcnpi  23564  txcmplem1  23597  tx1stc  23606  nrmr0reg  23705  fbssfi  23793  fbfinnfr  23797  fgcl  23834  ufinffr  23885  elfm2  23904  fmfnfmlem1  23910  fmco  23917  fbflim2  23933  flffbas  23951  flftg  23952  cnpflf2  23956  alexsubALT  24007  cnextcn  24023  isucn2  24234  ucnima  24236  blssexps  24382  blssex  24383  mopni3  24450  neibl  24457  metss  24464  metcnp3  24496  cfilucfil  24515  metustbl  24522  psmetutop  24523  mpomulcn  24826  rescncf  24858  lebnum  24931  xlebnum  24932  lebnumii  24933  lmmbr  25226  fgcfil  25239  ovolsslem  25453  ovolunlem1  25466  ovoliunnul  25476  itgcn  25814  ellimc3  25848  c1lip3  25972  itgsubstlem  26023  plyss  26172  ulmclm  26364  ulmcau  26372  ulmcn  26376  rlimcxp  26952  chtppilimlem2  27453  chtppilim  27454  madess  27874  lrrecfr  27951  midex  28821  umgrnloop0  29194  usgrnloop0ALT  29290  uhgr2edg  29293  vtxduhgr0nedg  29578  wlkonl1iedg  29749  elwspths2on  30047  elwspths2onw  30048  3cyclfrgrrn2  30374  isgrpo  30584  tpr2rico  34089  esumpcvgval  34255  omssubadd  34477  r1filim  35279  fineqvnttrclse  35299  connpconn  35448  cvmliftlem15  35511  cvmlift2lem10  35525  satfdmlem  35581  fmla1  35600  satffunlem1lem2  35616  satffunlem2lem2  35619  fnessref  36570  fvineqsneq  37664  pibt2  37669  ptrecube  37868  poimirlem29  37897  poimirlem30  37898  poimirlem31  37899  fdc1  37994  sstotbnd3  38024  totbndss  38025  heibor1lem  38057  heibor1  38058  opidonOLD  38100  rngmgmbs4  38179  lvoli2  39954  paddss2  40191  lhpexle1lem  40380  lhpexle2lem  40382  dvhdimlem  41817  dvh3dim3N  41822  mapdh9a  42162  hdmap11lem2  42215  fiphp3d  43173  pell1qrss14  43222  minregex  43887  mnuop3d  44624  grumnudlem  44638  ismnushort  44654  eliuniin  45455  restuni3  45474  eliuniin2  45476  disjrnmpt2  45544  rnmptbd2lem  45603  ssfiunibd  45668  supminfxrrnmpt  45826  climrec  45960  islptre  45976  lptre2pt  45995  limsupmnfuzlem  46081  limsupre3lem  46087  limsupvaluz2  46093  supcnvlimsup  46095  liminfvalxr  46138  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  stoweidlem27  46382  stoweidlem29  46384  stoweidlem35  46390  stoweidlem48  46403  stoweidlem62  46417  fourierdlem48  46509  fourierdlem64  46525  fourierdlem65  46526  fourierdlem71  46532  fourierdlem73  46534  fourierdlem94  46555  fourierdlem103  46564  fourierdlem104  46565  fourierdlem112  46573  fourierdlem113  46574  sge0isum  46782  sge0seq  46801  meaiuninclem  46835  carageniuncllem2  46877  ovnsslelem  46915  hoidmvlelem1  46950  2reuimp  47472  afvelima  47524  sgoldbeven3prm  48140  nnsum4primes4  48146  nnsum4primesprm  48148  nnsum4primesgbe  48150  nnsum4primesle9  48152  grtriprop  48298  pgrpgt2nabl  48723  opnneilv  49265  sepnsepo  49280