Theorem reximdv 3275

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  r19.12  3326  r19.12OLD  3329  ss2rexv  4038  reusv3  5308  fvelima  6733  iunpw  7495  frxp  7822  ssfi  8740  ordtypelem2  8985  wdom2d  9046  xpwdomg  9051  cff1  9682  iunfo  9963  nqereu  10353  reclem3pr  10473  map2psrpr  10534  supsrlem  10535  1re  10643  elss2prb  13848  exprelprel  13850  o1lo1  14896  rlimcn1  14947  subcn2  14953  lo1add  14985  lo1mul  14986  pythagtriplem19  16172  vdwnnlem2  16334  ramub2  16352  sylow2alem2  18745  lsmless2x  18772  efgrelexlemb  18878  scmateALT  21123  decpmatmulsumfsupp  21383  pmatcollpw1lem1  21384  pmatcollpw2lem  21387  pm2mpmhmlem1  21428  cpmidpmatlem3  21482  cpmidgsum2  21489  tgcl  21579  neiss  21719  ssnei2  21726  tgcnp  21863  cnpco  21877  cnpresti  21898  lmcnp  21914  hausnei2  21963  1stcrest  22063  nlly2i  22086  llyss  22089  nllyss  22090  reftr  22124  lfinun  22135  txcnpi  22218  txcmplem1  22251  tx1stc  22260  nrmr0reg  22359  fbssfi  22447  fbfinnfr  22451  fgcl  22488  ufinffr  22539  elfm2  22558  fmfnfmlem1  22564  fmco  22571  fbflim2  22587  flffbas  22605  flftg  22606  cnpflf2  22610  alexsubALT  22661  cnextcn  22677  isucn2  22890  ucnima  22892  blssexps  23038  blssex  23039  mopni3  23106  neibl  23113  metss  23120  metcnp3  23152  cfilucfil  23171  metustbl  23178  psmetutop  23179  rescncf  23507  lebnum  23570  xlebnum  23571  lebnumii  23572  lmmbr  23863  fgcfil  23876  ovolsslem  24087  ovolunlem1  24100  ovoliunnul  24110  itgcn  24445  ellimc3  24479  c1lip3  24598  itgsubstlem  24647  plyss  24791  ulmclm  24977  ulmcau  24985  ulmcn  24989  rlimcxp  25553  chtppilimlem2  26052  chtppilim  26053  midex  26525  umgrnloop0  26896  usgrnloop0ALT  26989  uhgr2edg  26992  vtxduhgr0nedg  27276  wlkonl1iedg  27449  elwspths2on  27741  3cyclfrgrrn2  28068  isgrpo  28276  tpr2rico  31157  esumpcvgval  31339  omssubadd  31560  connpconn  32484  cvmliftlem15  32547  cvmlift2lem10  32561  satfdmlem  32617  fmla1  32636  satffunlem1lem2  32652  satffunlem2lem2  32655  fnessref  33707  fvineqsneq  34695  pibt2  34700  ptrecube  34894  poimirlem29  34923  poimirlem30  34924  poimirlem31  34925  fdc1  35023  sstotbnd3  35056  totbndss  35057  heibor1lem  35089  heibor1  35090  opidonOLD  35132  rngmgmbs4  35211  lvoli2  36719  paddss2  36956  lhpexle1lem  37145  lhpexle2lem  37147  dvhdimlem  38582  dvh3dim3N  38587  mapdh9a  38927  hdmap11lem2  38980  fiphp3d  39423  pell1qrss14  39472  mnuop3d  40614  grumnudlem  40628  eliuniin  41372  restuni3  41391  eliuniin2  41393  disjrnmpt2  41456  rnmptbd2lem  41527  ssfiunibd  41583  supminfxrrnmpt  41754  climrec  41891  islptre  41907  lptre2pt  41928  limsupmnfuzlem  42014  limsupre3lem  42020  limsupvaluz2  42026  supcnvlimsup  42028  liminfvalxr  42071  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  stoweidlem27  42319  stoweidlem29  42321  stoweidlem35  42327  stoweidlem48  42340  stoweidlem62  42354  fourierdlem48  42446  fourierdlem64  42462  fourierdlem65  42463  fourierdlem71  42469  fourierdlem73  42471  fourierdlem94  42492  fourierdlem103  42501  fourierdlem104  42502  fourierdlem112  42510  fourierdlem113  42511  sge0isum  42716  sge0seq  42735  meaiuninclem  42769  carageniuncllem2  42811  ovnsslelem  42849  hoidmvlelem1  42884  2reuimp  43321  afvelima  43373  sgoldbeven3prm  43955  nnsum4primes4  43961  nnsum4primesprm  43963  nnsum4primesgbe  43965  nnsum4primesle9  43967  pgrpgt2nabl  44421