Theorem reximdv 3155

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  r19.12  3289  ss2rexv  3993  reusv3  5341  fvelima  6899  iunpw  7721  frxp  8073  nnaordex2  8572  ssfiALT  9105  ordtypelem2  9431  wdom2d  9492  xpwdomg  9497  cff1  10178  iunfo  10459  nqereu  10850  reclem3pr  10970  map2psrpr  11031  supsrlem  11032  1re  11142  elss2prb  14448  exprelprel  14450  o1lo1  15497  rlimcn1  15548  subcn2  15555  lo1add  15587  lo1mul  15588  pythagtriplem19  16802  vdwnnlem2  16965  ramub2  16983  sylow2alem2  19591  lsmless2x  19618  efgrelexlemb  19723  scmateALT  22502  decpmatmulsumfsupp  22763  pmatcollpw1lem1  22764  pmatcollpw2lem  22767  pm2mpmhmlem1  22808  cpmidpmatlem3  22862  cpmidgsum2  22869  tgcl  22959  neiss  23099  ssnei2  23106  tgcnp  23243  cnpco  23257  cnpresti  23278  lmcnp  23294  hausnei2  23343  1stcrest  23443  nlly2i  23466  llyss  23469  nllyss  23470  reftr  23504  lfinun  23515  txcnpi  23598  txcmplem1  23631  tx1stc  23640  nrmr0reg  23739  fbssfi  23827  fbfinnfr  23831  fgcl  23868  ufinffr  23919  elfm2  23938  fmfnfmlem1  23944  fmco  23951  fbflim2  23967  flffbas  23985  flftg  23986  cnpflf2  23990  alexsubALT  24041  cnextcn  24057  isucn2  24268  ucnima  24270  blssexps  24416  blssex  24417  mopni3  24484  neibl  24491  metss  24498  metcnp3  24530  cfilucfil  24549  metustbl  24556  psmetutop  24557  mpomulcn  24859  rescncf  24889  lebnum  24956  xlebnum  24957  lebnumii  24958  lmmbr  25250  fgcfil  25263  ovolsslem  25476  ovolunlem1  25489  ovoliunnul  25499  itgcn  25837  ellimc3  25871  c1lip3  25991  itgsubstlem  26040  plyss  26189  ulmclm  26377  ulmcau  26385  ulmcn  26389  rlimcxp  26962  chtppilimlem2  27462  chtppilim  27463  madess  27883  lrrecfr  27960  midex  28830  umgrnloop0  29203  usgrnloop0ALT  29299  uhgr2edg  29302  vtxduhgr0nedg  29586  wlkonl1iedg  29757  elwspths2on  30055  elwspths2onw  30056  3cyclfrgrrn2  30382  isgrpo  30593  tpr2rico  34103  esumpcvgval  34269  omssubadd  34491  r1filim  35292  fineqvnttrclse  35312  connpconn  35470  cvmliftlem15  35533  cvmlift2lem10  35547  satfdmlem  35603  fmla1  35622  satffunlem1lem2  35638  satffunlem2lem2  35641  fnessref  36592  ttctr  36728  fvineqsneq  37781  pibt2  37786  ptrecube  37994  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  fdc1  38120  sstotbnd3  38150  totbndss  38151  heibor1lem  38183  heibor1  38184  opidonOLD  38226  rngmgmbs4  38305  lvoli2  40080  paddss2  40317  lhpexle1lem  40506  lhpexle2lem  40508  dvhdimlem  41943  dvh3dim3N  41948  mapdh9a  42288  hdmap11lem2  42341  fiphp3d  43271  pell1qrss14  43320  minregex  43985  mnuop3d  44722  grumnudlem  44736  ismnushort  44752  eliuniin  45553  restuni3  45572  eliuniin2  45574  disjrnmpt2  45642  rnmptbd2lem  45699  ssfiunibd  45764  supminfxrrnmpt  45921  climrec  46055  islptre  46071  lptre2pt  46090  limsupmnfuzlem  46176  limsupre3lem  46182  limsupvaluz2  46188  supcnvlimsup  46190  liminfvalxr  46233  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stoweidlem27  46477  stoweidlem29  46479  stoweidlem35  46485  stoweidlem48  46498  stoweidlem62  46512  fourierdlem48  46604  fourierdlem64  46620  fourierdlem65  46621  fourierdlem71  46627  fourierdlem73  46629  fourierdlem94  46650  fourierdlem103  46659  fourierdlem104  46660  fourierdlem112  46668  fourierdlem113  46669  sge0isum  46877  sge0seq  46896  meaiuninclem  46930  carageniuncllem2  46972  ovnsslelem  47010  hoidmvlelem1  47045  2reuimp  47585  afvelima  47637  sgoldbeven3prm  48281  nnsum4primes4  48287  nnsum4primesprm  48289  nnsum4primesgbe  48291  nnsum4primesle9  48293  grtriprop  48439  pgrpgt2nabl  48864  opnneilv  49406  sepnsepo  49421