Theorem reximdv 3198

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

Syntax hints:   → wi 4   ∈ wcel 2112  ∃wrex 3072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-ral 3076  df-rex 3077

This theorem is referenced by:  r19.12  3249  ss2rexv  3962  reusv3  5275  fvelima  6720  iunpw  7493  frxp  7826  ssfi  8760  ordtypelem2  9009  wdom2d  9070  xpwdomg  9075  cff1  9711  iunfo  9992  nqereu  10382  reclem3pr  10502  map2psrpr  10563  supsrlem  10564  1re  10672  elss2prb  13890  exprelprel  13892  o1lo1  14935  rlimcn1  14986  subcn2  14992  lo1add  15024  lo1mul  15025  pythagtriplem19  16218  vdwnnlem2  16380  ramub2  16398  sylow2alem2  18803  lsmless2x  18830  efgrelexlemb  18936  scmateALT  21205  decpmatmulsumfsupp  21466  pmatcollpw1lem1  21467  pmatcollpw2lem  21470  pm2mpmhmlem1  21511  cpmidpmatlem3  21565  cpmidgsum2  21572  tgcl  21662  neiss  21802  ssnei2  21809  tgcnp  21946  cnpco  21960  cnpresti  21981  lmcnp  21997  hausnei2  22046  1stcrest  22146  nlly2i  22169  llyss  22172  nllyss  22173  reftr  22207  lfinun  22218  txcnpi  22301  txcmplem1  22334  tx1stc  22343  nrmr0reg  22442  fbssfi  22530  fbfinnfr  22534  fgcl  22571  ufinffr  22622  elfm2  22641  fmfnfmlem1  22647  fmco  22654  fbflim2  22670  flffbas  22688  flftg  22689  cnpflf2  22693  alexsubALT  22744  cnextcn  22760  isucn2  22973  ucnima  22975  blssexps  23121  blssex  23122  mopni3  23189  neibl  23196  metss  23203  metcnp3  23235  cfilucfil  23254  metustbl  23261  psmetutop  23262  rescncf  23591  lebnum  23658  xlebnum  23659  lebnumii  23660  lmmbr  23951  fgcfil  23964  ovolsslem  24177  ovolunlem1  24190  ovoliunnul  24200  itgcn  24537  ellimc3  24571  c1lip3  24691  itgsubstlem  24740  plyss  24888  ulmclm  25074  ulmcau  25082  ulmcn  25086  rlimcxp  25651  chtppilimlem2  26150  chtppilim  26151  midex  26623  umgrnloop0  26994  usgrnloop0ALT  27087  uhgr2edg  27090  vtxduhgr0nedg  27374  wlkonl1iedg  27547  elwspths2on  27838  3cyclfrgrrn2  28164  isgrpo  28372  tpr2rico  31376  esumpcvgval  31558  omssubadd  31779  connpconn  32706  cvmliftlem15  32769  cvmlift2lem10  32783  satfdmlem  32839  fmla1  32858  satffunlem1lem2  32874  satffunlem2lem2  32877  madess  33609  lrrecfr  33640  fnessref  34088  fvineqsneq  35102  pibt2  35107  ptrecube  35330  poimirlem29  35359  poimirlem30  35360  poimirlem31  35361  fdc1  35457  sstotbnd3  35487  totbndss  35488  heibor1lem  35520  heibor1  35521  opidonOLD  35563  rngmgmbs4  35642  lvoli2  37150  paddss2  37387  lhpexle1lem  37576  lhpexle2lem  37578  dvhdimlem  39013  dvh3dim3N  39018  mapdh9a  39358  hdmap11lem2  39411  sn-negex12  39888  fiphp3d  40126  pell1qrss14  40175  mnuop3d  41345  grumnudlem  41359  eliuniin  42101  restuni3  42119  eliuniin2  42121  disjrnmpt2  42178  rnmptbd2lem  42247  ssfiunibd  42302  supminfxrrnmpt  42469  climrec  42604  islptre  42620  lptre2pt  42641  limsupmnfuzlem  42727  limsupre3lem  42733  limsupvaluz2  42739  supcnvlimsup  42741  liminfvalxr  42784  ioodvbdlimc1lem2  42933  ioodvbdlimc2lem  42935  stoweidlem27  43028  stoweidlem29  43030  stoweidlem35  43036  stoweidlem48  43049  stoweidlem62  43063  fourierdlem48  43155  fourierdlem64  43171  fourierdlem65  43172  fourierdlem71  43178  fourierdlem73  43180  fourierdlem94  43201  fourierdlem103  43210  fourierdlem104  43211  fourierdlem112  43219  fourierdlem113  43220  sge0isum  43425  sge0seq  43444  meaiuninclem  43478  carageniuncllem2  43520  ovnsslelem  43558  hoidmvlelem1  43593  2reuimp  44032  afvelima  44084  sgoldbeven3prm  44661  nnsum4primes4  44667  nnsum4primesprm  44669  nnsum4primesgbe  44671  nnsum4primesle9  44673  pgrpgt2nabl  45128  opnneilv  45577  isnrm4lem3  45583