Theorem reximdv 3176

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  r19.12  3320  r19.12OLD  3321  ss2rexv  4080  reusv3  5423  fvelima  6987  iunpw  7806  frxp  8167  nnaordex2  8695  ssfiALT  9241  ordtypelem2  9588  wdom2d  9649  xpwdomg  9654  cff1  10327  iunfo  10608  nqereu  10998  reclem3pr  11118  map2psrpr  11179  supsrlem  11180  1re  11290  elss2prb  14537  exprelprel  14539  o1lo1  15583  rlimcn1  15634  subcn2  15641  lo1add  15673  lo1mul  15674  pythagtriplem19  16880  vdwnnlem2  17043  ramub2  17061  sylow2alem2  19660  lsmless2x  19687  efgrelexlemb  19792  scmateALT  22539  decpmatmulsumfsupp  22800  pmatcollpw1lem1  22801  pmatcollpw2lem  22804  pm2mpmhmlem1  22845  cpmidpmatlem3  22899  cpmidgsum2  22906  tgcl  22997  neiss  23138  ssnei2  23145  tgcnp  23282  cnpco  23296  cnpresti  23317  lmcnp  23333  hausnei2  23382  1stcrest  23482  nlly2i  23505  llyss  23508  nllyss  23509  reftr  23543  lfinun  23554  txcnpi  23637  txcmplem1  23670  tx1stc  23679  nrmr0reg  23778  fbssfi  23866  fbfinnfr  23870  fgcl  23907  ufinffr  23958  elfm2  23977  fmfnfmlem1  23983  fmco  23990  fbflim2  24006  flffbas  24024  flftg  24025  cnpflf2  24029  alexsubALT  24080  cnextcn  24096  isucn2  24309  ucnima  24311  blssexps  24457  blssex  24458  mopni3  24528  neibl  24535  metss  24542  metcnp3  24574  cfilucfil  24593  metustbl  24600  psmetutop  24601  mpomulcn  24910  rescncf  24942  lebnum  25015  xlebnum  25016  lebnumii  25017  lmmbr  25311  fgcfil  25324  ovolsslem  25538  ovolunlem1  25551  ovoliunnul  25561  itgcn  25900  ellimc3  25934  c1lip3  26058  itgsubstlem  26109  plyss  26258  ulmclm  26448  ulmcau  26456  ulmcn  26460  rlimcxp  27035  chtppilimlem2  27536  chtppilim  27537  madess  27933  lrrecfr  27994  midex  28763  umgrnloop0  29144  usgrnloop0ALT  29240  uhgr2edg  29243  vtxduhgr0nedg  29528  wlkonl1iedg  29701  elwspths2on  29993  3cyclfrgrrn2  30319  isgrpo  30529  tpr2rico  33858  esumpcvgval  34042  omssubadd  34265  connpconn  35203  cvmliftlem15  35266  cvmlift2lem10  35280  satfdmlem  35336  fmla1  35355  satffunlem1lem2  35371  satffunlem2lem2  35374  fnessref  36323  fvineqsneq  37378  pibt2  37383  ptrecube  37580  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  fdc1  37706  sstotbnd3  37736  totbndss  37737  heibor1lem  37769  heibor1  37770  opidonOLD  37812  rngmgmbs4  37891  lvoli2  39538  paddss2  39775  lhpexle1lem  39964  lhpexle2lem  39966  dvhdimlem  41401  dvh3dim3N  41406  mapdh9a  41746  hdmap11lem2  41799  fiphp3d  42775  pell1qrss14  42824  minregex  43496  mnuop3d  44240  grumnudlem  44254  ismnushort  44270  eliuniin  45001  restuni3  45020  eliuniin2  45022  disjrnmpt2  45095  rnmptbd2lem  45157  ssfiunibd  45224  supminfxrrnmpt  45386  climrec  45524  islptre  45540  lptre2pt  45561  limsupmnfuzlem  45647  limsupre3lem  45653  limsupvaluz2  45659  supcnvlimsup  45661  liminfvalxr  45704  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem27  45948  stoweidlem29  45950  stoweidlem35  45956  stoweidlem48  45969  stoweidlem62  45983  fourierdlem48  46075  fourierdlem64  46091  fourierdlem65  46092  fourierdlem71  46098  fourierdlem73  46100  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem113  46140  sge0isum  46348  sge0seq  46367  meaiuninclem  46401  carageniuncllem2  46443  ovnsslelem  46481  hoidmvlelem1  46516  2reuimp  47030  afvelima  47082  sgoldbeven3prm  47657  nnsum4primes4  47663  nnsum4primesprm  47665  nnsum4primesgbe  47667  nnsum4primesle9  47669  grtriprop  47792  pgrpgt2nabl  48091  opnneilv  48588  sepnsepo  48603