Theorem reximdv 3160

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

Syntax hints:   → wi 4   ∈ wcel 2099  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-rex 3061

This theorem is referenced by:  r19.12  3302  r19.12OLD  3303  ss2rexv  4051  reusv3  5409  fvelima  6968  iunpw  7779  frxp  8140  nnaordex2  8669  ssfiALT  9212  ordtypelem2  9562  wdom2d  9623  xpwdomg  9628  cff1  10301  iunfo  10582  nqereu  10972  reclem3pr  11092  map2psrpr  11153  supsrlem  11154  1re  11264  elss2prb  14506  exprelprel  14508  o1lo1  15539  rlimcn1  15590  subcn2  15597  lo1add  15629  lo1mul  15630  pythagtriplem19  16835  vdwnnlem2  16998  ramub2  17016  sylow2alem2  19616  lsmless2x  19643  efgrelexlemb  19748  scmateALT  22505  decpmatmulsumfsupp  22766  pmatcollpw1lem1  22767  pmatcollpw2lem  22770  pm2mpmhmlem1  22811  cpmidpmatlem3  22865  cpmidgsum2  22872  tgcl  22963  neiss  23104  ssnei2  23111  tgcnp  23248  cnpco  23262  cnpresti  23283  lmcnp  23299  hausnei2  23348  1stcrest  23448  nlly2i  23471  llyss  23474  nllyss  23475  reftr  23509  lfinun  23520  txcnpi  23603  txcmplem1  23636  tx1stc  23645  nrmr0reg  23744  fbssfi  23832  fbfinnfr  23836  fgcl  23873  ufinffr  23924  elfm2  23943  fmfnfmlem1  23949  fmco  23956  fbflim2  23972  flffbas  23990  flftg  23991  cnpflf2  23995  alexsubALT  24046  cnextcn  24062  isucn2  24275  ucnima  24277  blssexps  24423  blssex  24424  mopni3  24494  neibl  24501  metss  24508  metcnp3  24540  cfilucfil  24559  metustbl  24566  psmetutop  24567  mpomulcn  24876  rescncf  24908  lebnum  24981  xlebnum  24982  lebnumii  24983  lmmbr  25277  fgcfil  25290  ovolsslem  25504  ovolunlem1  25517  ovoliunnul  25527  itgcn  25865  ellimc3  25899  c1lip3  26023  itgsubstlem  26074  plyss  26226  ulmclm  26416  ulmcau  26424  ulmcn  26428  rlimcxp  27002  chtppilimlem2  27503  chtppilim  27504  madess  27900  lrrecfr  27957  midex  28664  umgrnloop0  29045  usgrnloop0ALT  29141  uhgr2edg  29144  vtxduhgr0nedg  29429  wlkonl1iedg  29602  elwspths2on  29894  3cyclfrgrrn2  30220  isgrpo  30430  tpr2rico  33727  esumpcvgval  33911  omssubadd  34134  connpconn  35063  cvmliftlem15  35126  cvmlift2lem10  35140  satfdmlem  35196  fmla1  35215  satffunlem1lem2  35231  satffunlem2lem2  35234  fnessref  36069  fvineqsneq  37119  pibt2  37124  ptrecube  37321  poimirlem29  37350  poimirlem30  37351  poimirlem31  37352  fdc1  37447  sstotbnd3  37477  totbndss  37478  heibor1lem  37510  heibor1  37511  opidonOLD  37553  rngmgmbs4  37632  lvoli2  39280  paddss2  39517  lhpexle1lem  39706  lhpexle2lem  39708  dvhdimlem  41143  dvh3dim3N  41148  mapdh9a  41488  hdmap11lem2  41541  sn-negex12  42196  fiphp3d  42476  pell1qrss14  42525  minregex  43201  mnuop3d  43945  grumnudlem  43959  ismnushort  43975  eliuniin  44700  restuni3  44719  eliuniin2  44721  disjrnmpt2  44795  rnmptbd2lem  44857  ssfiunibd  44924  supminfxrrnmpt  45086  climrec  45224  islptre  45240  lptre2pt  45261  limsupmnfuzlem  45347  limsupre3lem  45353  limsupvaluz2  45359  supcnvlimsup  45361  liminfvalxr  45404  ioodvbdlimc1lem2  45553  ioodvbdlimc2lem  45555  stoweidlem27  45648  stoweidlem29  45650  stoweidlem35  45656  stoweidlem48  45669  stoweidlem62  45683  fourierdlem48  45775  fourierdlem64  45791  fourierdlem65  45792  fourierdlem71  45798  fourierdlem73  45800  fourierdlem94  45821  fourierdlem103  45830  fourierdlem104  45831  fourierdlem112  45839  fourierdlem113  45840  sge0isum  46048  sge0seq  46067  meaiuninclem  46101  carageniuncllem2  46143  ovnsslelem  46181  hoidmvlelem1  46216  2reuimp  46728  afvelima  46780  sgoldbeven3prm  47355  nnsum4primes4  47361  nnsum4primesprm  47363  nnsum4primesgbe  47365  nnsum4primesle9  47367  pgrpgt2nabl  47745  opnneilv  48242  sepnsepo  48257