Theorem reximdv 3148

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3057

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  r19.12  3282  ss2rexv  4002  reusv3  5347  fvelima  6896  iunpw  7713  frxp  8065  nnaordex2  8563  ssfiALT  9094  ordtypelem2  9416  wdom2d  9477  xpwdomg  9482  cff1  10160  iunfo  10441  nqereu  10831  reclem3pr  10951  map2psrpr  11012  supsrlem  11013  1re  11123  elss2prb  14402  exprelprel  14404  o1lo1  15451  rlimcn1  15502  subcn2  15509  lo1add  15541  lo1mul  15542  pythagtriplem19  16752  vdwnnlem2  16915  ramub2  16933  sylow2alem2  19538  lsmless2x  19565  efgrelexlemb  19670  scmateALT  22447  decpmatmulsumfsupp  22708  pmatcollpw1lem1  22709  pmatcollpw2lem  22712  pm2mpmhmlem1  22753  cpmidpmatlem3  22807  cpmidgsum2  22814  tgcl  22904  neiss  23044  ssnei2  23051  tgcnp  23188  cnpco  23202  cnpresti  23223  lmcnp  23239  hausnei2  23288  1stcrest  23388  nlly2i  23411  llyss  23414  nllyss  23415  reftr  23449  lfinun  23460  txcnpi  23543  txcmplem1  23576  tx1stc  23585  nrmr0reg  23684  fbssfi  23772  fbfinnfr  23776  fgcl  23813  ufinffr  23864  elfm2  23883  fmfnfmlem1  23889  fmco  23896  fbflim2  23912  flffbas  23930  flftg  23931  cnpflf2  23935  alexsubALT  23986  cnextcn  24002  isucn2  24213  ucnima  24215  blssexps  24361  blssex  24362  mopni3  24429  neibl  24436  metss  24443  metcnp3  24475  cfilucfil  24494  metustbl  24501  psmetutop  24502  mpomulcn  24805  rescncf  24837  lebnum  24910  xlebnum  24911  lebnumii  24912  lmmbr  25205  fgcfil  25218  ovolsslem  25432  ovolunlem1  25445  ovoliunnul  25455  itgcn  25793  ellimc3  25827  c1lip3  25951  itgsubstlem  26002  plyss  26151  ulmclm  26343  ulmcau  26351  ulmcn  26355  rlimcxp  26931  chtppilimlem2  27432  chtppilim  27433  madess  27841  lrrecfr  27906  midex  28735  umgrnloop0  29108  usgrnloop0ALT  29204  uhgr2edg  29207  vtxduhgr0nedg  29492  wlkonl1iedg  29663  elwspths2on  29961  elwspths2onw  29962  3cyclfrgrrn2  30288  isgrpo  30498  tpr2rico  33997  esumpcvgval  34163  omssubadd  34385  r1filim  35187  fineqvnttrclse  35216  connpconn  35351  cvmliftlem15  35414  cvmlift2lem10  35428  satfdmlem  35484  fmla1  35503  satffunlem1lem2  35519  satffunlem2lem2  35522  fnessref  36473  fvineqsneq  37529  pibt2  37534  ptrecube  37733  poimirlem29  37762  poimirlem30  37763  poimirlem31  37764  fdc1  37859  sstotbnd3  37889  totbndss  37890  heibor1lem  37922  heibor1  37923  opidonOLD  37965  rngmgmbs4  38044  lvoli2  39753  paddss2  39990  lhpexle1lem  40179  lhpexle2lem  40181  dvhdimlem  41616  dvh3dim3N  41621  mapdh9a  41961  hdmap11lem2  42014  fiphp3d  42976  pell1qrss14  43025  minregex  43691  mnuop3d  44428  grumnudlem  44442  ismnushort  44458  eliuniin  45259  restuni3  45278  eliuniin2  45280  disjrnmpt2  45348  rnmptbd2lem  45408  ssfiunibd  45473  supminfxrrnmpt  45631  climrec  45765  islptre  45781  lptre2pt  45800  limsupmnfuzlem  45886  limsupre3lem  45892  limsupvaluz2  45898  supcnvlimsup  45900  liminfvalxr  45943  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  stoweidlem27  46187  stoweidlem29  46189  stoweidlem35  46195  stoweidlem48  46208  stoweidlem62  46222  fourierdlem48  46314  fourierdlem64  46330  fourierdlem65  46331  fourierdlem71  46337  fourierdlem73  46339  fourierdlem94  46360  fourierdlem103  46369  fourierdlem104  46370  fourierdlem112  46378  fourierdlem113  46379  sge0isum  46587  sge0seq  46606  meaiuninclem  46640  carageniuncllem2  46682  ovnsslelem  46720  hoidmvlelem1  46755  2reuimp  47277  afvelima  47329  sgoldbeven3prm  47945  nnsum4primes4  47951  nnsum4primesprm  47953  nnsum4primesgbe  47955  nnsum4primesle9  47957  grtriprop  48103  pgrpgt2nabl  48528  opnneilv  49070  sepnsepo  49085