Theorem reximdv 2999

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
reximdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		reximdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 2998	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  r19.12  3045  reusv3  4802  fvelima  6158  iunpw  6870  frxp  7174  ssfi  8065  ordtypelem2  8307  wdom2d  8368  xpwdomg  8373  cff1  8963  iunfo  9240  nqereu  9630  reclem3pr  9750  map2psrpr  9810  supsrlem  9811  1re  9918  elss2prb  13123  exprelprel  13126  o1lo1  14116  rlimcn1  14167  subcn2  14173  lo1add  14205  lo1mul  14206  pythagtriplem19  15376  vdwnnlem2  15538  ramub2  15556  sylow2alem2  17856  lsmless2x  17883  efgrelexlemb  17986  scmateALT  20137  decpmatmulsumfsupp  20397  pmatcollpw1lem1  20398  pmatcollpw2lem  20401  pm2mpmhmlem1  20442  cpmidpmatlem3  20496  cpmidgsum2  20503  tgcl  20584  neiss  20723  ssnei2  20730  tgcnp  20867  cnpco  20881  cnpresti  20902  lmcnp  20918  hausnei2  20967  1stcrest  21066  nlly2i  21089  llyss  21092  nllyss  21093  reftr  21127  lfinun  21138  txcnpi  21221  txcmplem1  21254  tx1stc  21263  nrmr0reg  21362  fbssfi  21451  fbfinnfr  21455  fgcl  21492  ufinffr  21543  elfm2  21562  fmfnfmlem1  21568  fmco  21575  fbflim2  21591  flffbas  21609  flftg  21610  cnpflf2  21614  alexsubALT  21665  cnextcn  21681  isucn2  21893  ucnima  21895  blssexps  22041  blssex  22042  mopni3  22109  neibl  22116  metss  22123  metcnp3  22155  cfilucfil  22174  metustbl  22181  psmetutop  22182  rescncf  22508  lebnum  22571  xlebnum  22572  lebnumii  22573  lmmbr  22864  fgcfil  22877  ovolsslem  23059  ovolunlem1  23072  ovoliunnul  23082  itgcn  23415  ellimc3  23449  c1lip3  23566  itgsubstlem  23615  plyss  23759  ulmclm  23945  ulmcau  23953  ulmcn  23957  rlimcxp  24500  chtppilimlem2  24963  chtppilim  24964  midex  25429  umgrnloop0  25775  usgranloop0  25909  usgra2edg  25911  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  vdusgra0nedg  26435  usgravd0nedg  26445  3cyclfrgrarn2  26541  vdn0frgrav2  26550  vdgn0frgrav2  26551  frgrawopreg1  26577  frgrawopreg2  26578  isgrpo  26735  tpr2rico  29286  esumpcvgval  29467  omssubadd  29689  conpcon  30471  cvmliftlem15  30534  cvmlift2lem10  30548  fnessref  31522  ptrecube  32579  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  fdc1  32712  sstotbnd3  32745  totbndss  32746  heibor1lem  32778  heibor1  32779  opidonOLD  32821  rngmgmbs4  32900  lvoli2  33885  paddss2  34122  lhpexle1lem  34311  lhpexle2lem  34313  dvhdimlem  35751  dvh3dim3N  35756  mapdh9a  36097  hdmap11lem2  36152  fiphp3d  36401  pell1qrss14  36450  eliuniin  38307  restuni3  38333  eliuniin2  38335  disjrnmpt2  38370  ssfiunibd  38464  climrec  38670  islptre  38686  lptre2pt  38707  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem27  38920  stoweidlem29  38922  stoweidlem35  38928  stoweidlem48  38941  stoweidlem62  38955  fourierdlem48  39047  fourierdlem64  39063  fourierdlem65  39064  fourierdlem71  39070  fourierdlem73  39072  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  sge0isum  39320  sge0seq  39339  meaiuninclem  39373  carageniuncllem2  39412  ovnsslelem  39450  hoidmvlelem1  39485  afvelima  39896  nnsum4primes4  40205  nnsum4primesprm  40207  nnsum4primesgbe  40209  nnsum4primesle9  40211  usgrnloop0ALT  40432  uhgr2edg  40435  vtxduhgr0nedg  40707  wlkOnl1iedg  40873  elwspths2on  41163  3cyclfrgrrn2  41457  frgrwopreg1  41487  frgrwopreg2  41488  pgrpgt2nabl  41941