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  3288  ss2rexv  4018  reusv3  5360  fvelima  6926  iunpw  7747  frxp  8105  nnaordex2  8603  ssfiALT  9138  ordtypelem2  9472  wdom2d  9533  xpwdomg  9538  cff1  10211  iunfo  10492  nqereu  10882  reclem3pr  11002  map2psrpr  11063  supsrlem  11064  1re  11174  elss2prb  14453  exprelprel  14455  o1lo1  15503  rlimcn1  15554  subcn2  15561  lo1add  15593  lo1mul  15594  pythagtriplem19  16804  vdwnnlem2  16967  ramub2  16985  sylow2alem2  19548  lsmless2x  19575  efgrelexlemb  19680  scmateALT  22399  decpmatmulsumfsupp  22660  pmatcollpw1lem1  22661  pmatcollpw2lem  22664  pm2mpmhmlem1  22705  cpmidpmatlem3  22759  cpmidgsum2  22766  tgcl  22856  neiss  22996  ssnei2  23003  tgcnp  23140  cnpco  23154  cnpresti  23175  lmcnp  23191  hausnei2  23240  1stcrest  23340  nlly2i  23363  llyss  23366  nllyss  23367  reftr  23401  lfinun  23412  txcnpi  23495  txcmplem1  23528  tx1stc  23537  nrmr0reg  23636  fbssfi  23724  fbfinnfr  23728  fgcl  23765  ufinffr  23816  elfm2  23835  fmfnfmlem1  23841  fmco  23848  fbflim2  23864  flffbas  23882  flftg  23883  cnpflf2  23887  alexsubALT  23938  cnextcn  23954  isucn2  24166  ucnima  24168  blssexps  24314  blssex  24315  mopni3  24382  neibl  24389  metss  24396  metcnp3  24428  cfilucfil  24447  metustbl  24454  psmetutop  24455  mpomulcn  24758  rescncf  24790  lebnum  24863  xlebnum  24864  lebnumii  24865  lmmbr  25158  fgcfil  25171  ovolsslem  25385  ovolunlem1  25398  ovoliunnul  25408  itgcn  25746  ellimc3  25780  c1lip3  25904  itgsubstlem  25955  plyss  26104  ulmclm  26296  ulmcau  26304  ulmcn  26308  rlimcxp  26884  chtppilimlem2  27385  chtppilim  27386  madess  27788  lrrecfr  27850  midex  28664  umgrnloop0  29036  usgrnloop0ALT  29132  uhgr2edg  29135  vtxduhgr0nedg  29420  wlkonl1iedg  29593  elwspths2on  29890  3cyclfrgrrn2  30216  isgrpo  30426  tpr2rico  33902  esumpcvgval  34068  omssubadd  34291  connpconn  35222  cvmliftlem15  35285  cvmlift2lem10  35299  satfdmlem  35355  fmla1  35374  satffunlem1lem2  35390  satffunlem2lem2  35393  fnessref  36345  fvineqsneq  37400  pibt2  37405  ptrecube  37614  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  fdc1  37740  sstotbnd3  37770  totbndss  37771  heibor1lem  37803  heibor1  37804  opidonOLD  37846  rngmgmbs4  37925  lvoli2  39575  paddss2  39812  lhpexle1lem  40001  lhpexle2lem  40003  dvhdimlem  41438  dvh3dim3N  41443  mapdh9a  41783  hdmap11lem2  41836  fiphp3d  42807  pell1qrss14  42856  minregex  43523  mnuop3d  44260  grumnudlem  44274  ismnushort  44290  eliuniin  45093  restuni3  45112  eliuniin2  45114  disjrnmpt2  45182  rnmptbd2lem  45242  ssfiunibd  45307  supminfxrrnmpt  45467  climrec  45601  islptre  45617  lptre2pt  45638  limsupmnfuzlem  45724  limsupre3lem  45730  limsupvaluz2  45736  supcnvlimsup  45738  liminfvalxr  45781  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem27  46025  stoweidlem29  46027  stoweidlem35  46033  stoweidlem48  46046  stoweidlem62  46060  fourierdlem48  46152  fourierdlem64  46168  fourierdlem65  46169  fourierdlem71  46175  fourierdlem73  46177  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  sge0isum  46425  sge0seq  46444  meaiuninclem  46478  carageniuncllem2  46520  ovnsslelem  46558  hoidmvlelem1  46593  2reuimp  47116  afvelima  47168  sgoldbeven3prm  47784  nnsum4primes4  47790  nnsum4primesprm  47792  nnsum4primesgbe  47794  nnsum4primesle9  47796  grtriprop  47940  pgrpgt2nabl  48354  opnneilv  48897  sepnsepo  48912