Theorem reximdv 3167

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  r19.12  3311  r19.12OLD  3312  ss2rexv  4066  reusv3  5410  fvelima  6973  iunpw  7789  frxp  8149  nnaordex2  8675  ssfiALT  9212  ordtypelem2  9556  wdom2d  9617  xpwdomg  9622  cff1  10295  iunfo  10576  nqereu  10966  reclem3pr  11086  map2psrpr  11147  supsrlem  11148  1re  11258  elss2prb  14523  exprelprel  14525  o1lo1  15569  rlimcn1  15620  subcn2  15627  lo1add  15659  lo1mul  15660  pythagtriplem19  16866  vdwnnlem2  17029  ramub2  17047  sylow2alem2  19650  lsmless2x  19677  efgrelexlemb  19782  scmateALT  22533  decpmatmulsumfsupp  22794  pmatcollpw1lem1  22795  pmatcollpw2lem  22798  pm2mpmhmlem1  22839  cpmidpmatlem3  22893  cpmidgsum2  22900  tgcl  22991  neiss  23132  ssnei2  23139  tgcnp  23276  cnpco  23290  cnpresti  23311  lmcnp  23327  hausnei2  23376  1stcrest  23476  nlly2i  23499  llyss  23502  nllyss  23503  reftr  23537  lfinun  23548  txcnpi  23631  txcmplem1  23664  tx1stc  23673  nrmr0reg  23772  fbssfi  23860  fbfinnfr  23864  fgcl  23901  ufinffr  23952  elfm2  23971  fmfnfmlem1  23977  fmco  23984  fbflim2  24000  flffbas  24018  flftg  24019  cnpflf2  24023  alexsubALT  24074  cnextcn  24090  isucn2  24303  ucnima  24305  blssexps  24451  blssex  24452  mopni3  24522  neibl  24529  metss  24536  metcnp3  24568  cfilucfil  24587  metustbl  24594  psmetutop  24595  mpomulcn  24904  rescncf  24936  lebnum  25009  xlebnum  25010  lebnumii  25011  lmmbr  25305  fgcfil  25318  ovolsslem  25532  ovolunlem1  25545  ovoliunnul  25555  itgcn  25894  ellimc3  25928  c1lip3  26052  itgsubstlem  26103  plyss  26252  ulmclm  26444  ulmcau  26452  ulmcn  26456  rlimcxp  27031  chtppilimlem2  27532  chtppilim  27533  madess  27929  lrrecfr  27990  midex  28759  umgrnloop0  29140  usgrnloop0ALT  29236  uhgr2edg  29239  vtxduhgr0nedg  29524  wlkonl1iedg  29697  elwspths2on  29989  3cyclfrgrrn2  30315  isgrpo  30525  tpr2rico  33872  esumpcvgval  34058  omssubadd  34281  connpconn  35219  cvmliftlem15  35282  cvmlift2lem10  35296  satfdmlem  35352  fmla1  35371  satffunlem1lem2  35387  satffunlem2lem2  35390  fnessref  36339  fvineqsneq  37394  pibt2  37399  ptrecube  37606  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  fdc1  37732  sstotbnd3  37762  totbndss  37763  heibor1lem  37795  heibor1  37796  opidonOLD  37838  rngmgmbs4  37917  lvoli2  39563  paddss2  39800  lhpexle1lem  39989  lhpexle2lem  39991  dvhdimlem  41426  dvh3dim3N  41431  mapdh9a  41771  hdmap11lem2  41824  fiphp3d  42806  pell1qrss14  42855  minregex  43523  mnuop3d  44266  grumnudlem  44280  ismnushort  44296  eliuniin  45038  restuni3  45057  eliuniin2  45059  disjrnmpt2  45130  rnmptbd2lem  45192  ssfiunibd  45259  supminfxrrnmpt  45420  climrec  45558  islptre  45574  lptre2pt  45595  limsupmnfuzlem  45681  limsupre3lem  45687  limsupvaluz2  45693  supcnvlimsup  45695  liminfvalxr  45738  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem27  45982  stoweidlem29  45984  stoweidlem35  45990  stoweidlem48  46003  stoweidlem62  46017  fourierdlem48  46109  fourierdlem64  46125  fourierdlem65  46126  fourierdlem71  46132  fourierdlem73  46134  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem113  46174  sge0isum  46382  sge0seq  46401  meaiuninclem  46435  carageniuncllem2  46477  ovnsslelem  46515  hoidmvlelem1  46550  2reuimp  47064  afvelima  47116  sgoldbeven3prm  47707  nnsum4primes4  47713  nnsum4primesprm  47715  nnsum4primesgbe  47717  nnsum4primesle9  47719  grtriprop  47845  pgrpgt2nabl  48210  opnneilv  48704  sepnsepo  48719