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 2109  ∃wrex 3053

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 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.12  3285  ss2rexv  4015  reusv3  5355  fvelima  6908  iunpw  7727  frxp  8082  nnaordex2  8580  ssfiALT  9115  ordtypelem2  9448  wdom2d  9509  xpwdomg  9514  cff1  10187  iunfo  10468  nqereu  10858  reclem3pr  10978  map2psrpr  11039  supsrlem  11040  1re  11150  elss2prb  14429  exprelprel  14431  o1lo1  15479  rlimcn1  15530  subcn2  15537  lo1add  15569  lo1mul  15570  pythagtriplem19  16780  vdwnnlem2  16943  ramub2  16961  sylow2alem2  19524  lsmless2x  19551  efgrelexlemb  19656  scmateALT  22375  decpmatmulsumfsupp  22636  pmatcollpw1lem1  22637  pmatcollpw2lem  22640  pm2mpmhmlem1  22681  cpmidpmatlem3  22735  cpmidgsum2  22742  tgcl  22832  neiss  22972  ssnei2  22979  tgcnp  23116  cnpco  23130  cnpresti  23151  lmcnp  23167  hausnei2  23216  1stcrest  23316  nlly2i  23339  llyss  23342  nllyss  23343  reftr  23377  lfinun  23388  txcnpi  23471  txcmplem1  23504  tx1stc  23513  nrmr0reg  23612  fbssfi  23700  fbfinnfr  23704  fgcl  23741  ufinffr  23792  elfm2  23811  fmfnfmlem1  23817  fmco  23824  fbflim2  23840  flffbas  23858  flftg  23859  cnpflf2  23863  alexsubALT  23914  cnextcn  23930  isucn2  24142  ucnima  24144  blssexps  24290  blssex  24291  mopni3  24358  neibl  24365  metss  24372  metcnp3  24404  cfilucfil  24423  metustbl  24430  psmetutop  24431  mpomulcn  24734  rescncf  24766  lebnum  24839  xlebnum  24840  lebnumii  24841  lmmbr  25134  fgcfil  25147  ovolsslem  25361  ovolunlem1  25374  ovoliunnul  25384  itgcn  25722  ellimc3  25756  c1lip3  25880  itgsubstlem  25931  plyss  26080  ulmclm  26272  ulmcau  26280  ulmcn  26284  rlimcxp  26860  chtppilimlem2  27361  chtppilim  27362  madess  27764  lrrecfr  27826  midex  28640  umgrnloop0  29012  usgrnloop0ALT  29108  uhgr2edg  29111  vtxduhgr0nedg  29396  wlkonl1iedg  29567  elwspths2on  29863  3cyclfrgrrn2  30189  isgrpo  30399  tpr2rico  33875  esumpcvgval  34041  omssubadd  34264  connpconn  35195  cvmliftlem15  35258  cvmlift2lem10  35272  satfdmlem  35328  fmla1  35347  satffunlem1lem2  35363  satffunlem2lem2  35366  fnessref  36318  fvineqsneq  37373  pibt2  37378  ptrecube  37587  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  fdc1  37713  sstotbnd3  37743  totbndss  37744  heibor1lem  37776  heibor1  37777  opidonOLD  37819  rngmgmbs4  37898  lvoli2  39548  paddss2  39785  lhpexle1lem  39974  lhpexle2lem  39976  dvhdimlem  41411  dvh3dim3N  41416  mapdh9a  41756  hdmap11lem2  41809  fiphp3d  42780  pell1qrss14  42829  minregex  43496  mnuop3d  44233  grumnudlem  44247  ismnushort  44263  eliuniin  45066  restuni3  45085  eliuniin2  45087  disjrnmpt2  45155  rnmptbd2lem  45215  ssfiunibd  45280  supminfxrrnmpt  45440  climrec  45574  islptre  45590  lptre2pt  45611  limsupmnfuzlem  45697  limsupre3lem  45703  limsupvaluz2  45709  supcnvlimsup  45711  liminfvalxr  45754  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  stoweidlem27  45998  stoweidlem29  46000  stoweidlem35  46006  stoweidlem48  46019  stoweidlem62  46033  fourierdlem48  46125  fourierdlem64  46141  fourierdlem65  46142  fourierdlem71  46148  fourierdlem73  46150  fourierdlem94  46171  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  fourierdlem113  46190  sge0isum  46398  sge0seq  46417  meaiuninclem  46451  carageniuncllem2  46493  ovnsslelem  46531  hoidmvlelem1  46566  2reuimp  47089  afvelima  47141  sgoldbeven3prm  47757  nnsum4primes4  47763  nnsum4primesprm  47765  nnsum4primesgbe  47767  nnsum4primesle9  47769  grtriprop  47913  pgrpgt2nabl  48327  opnneilv  48870  sepnsepo  48885