Theorem reximdv 3162

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

Syntax hints:   → wi 4   ∈ wcel 2155  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061

This theorem is referenced by:  r19.12  3210  reusv3  5040  fvelima  6437  iunpw  7176  frxp  7489  ssfi  8387  ordtypelem2  8631  wdom2d  8692  xpwdomg  8697  cff1  9333  iunfo  9614  nqereu  10004  reclem3pr  10124  map2psrpr  10184  supsrlem  10185  1re  10293  elss2prb  13470  exprelprel  13472  o1lo1  14555  rlimcn1  14606  subcn2  14612  lo1add  14644  lo1mul  14645  pythagtriplem19  15819  vdwnnlem2  15981  ramub2  15999  sylow2alem2  18299  lsmless2x  18326  efgrelexlemb  18429  scmateALT  20595  decpmatmulsumfsupp  20857  pmatcollpw1lem1  20858  pmatcollpw2lem  20861  pm2mpmhmlem1  20902  cpmidpmatlem3  20956  cpmidgsum2  20963  tgcl  21053  neiss  21193  ssnei2  21200  tgcnp  21337  cnpco  21351  cnpresti  21372  lmcnp  21388  hausnei2  21437  1stcrest  21536  nlly2i  21559  llyss  21562  nllyss  21563  reftr  21597  lfinun  21608  txcnpi  21691  txcmplem1  21724  tx1stc  21733  nrmr0reg  21832  fbssfi  21920  fbfinnfr  21924  fgcl  21961  ufinffr  22012  elfm2  22031  fmfnfmlem1  22037  fmco  22044  fbflim2  22060  flffbas  22078  flftg  22079  cnpflf2  22083  alexsubALT  22134  cnextcn  22150  isucn2  22362  ucnima  22364  blssexps  22510  blssex  22511  mopni3  22578  neibl  22585  metss  22592  metcnp3  22624  cfilucfil  22643  metustbl  22650  psmetutop  22651  rescncf  22979  lebnum  23042  xlebnum  23043  lebnumii  23044  lmmbr  23335  fgcfil  23348  ovolsslem  23542  ovolunlem1  23555  ovoliunnul  23565  itgcn  23900  ellimc3  23934  c1lip3  24053  itgsubstlem  24102  plyss  24246  ulmclm  24432  ulmcau  24440  ulmcn  24444  rlimcxp  24991  chtppilimlem2  25454  chtppilim  25455  midex  25920  umgrnloop0  26281  usgrnloop0ALT  26375  uhgr2edg  26378  vtxduhgr0nedg  26679  wlkonl1iedg  26852  elwspths2on  27164  3cyclfrgrrn2  27525  isgrpo  27743  tpr2rico  30340  esumpcvgval  30522  omssubadd  30744  connpconn  31597  cvmliftlem15  31660  cvmlift2lem10  31674  fnessref  32727  ptrecube  33765  poimirlem29  33794  poimirlem30  33795  poimirlem31  33796  fdc1  33896  sstotbnd3  33929  totbndss  33930  heibor1lem  33962  heibor1  33963  opidonOLD  34005  rngmgmbs4  34084  lvoli2  35469  paddss2  35706  lhpexle1lem  35895  lhpexle2lem  35897  dvhdimlem  37332  dvh3dim3N  37337  mapdh9a  37677  hdmap11lem2  37730  fiphp3d  37993  pell1qrss14  38042  eliuniin  39862  restuni3  39883  eliuniin2  39885  disjrnmpt2  39954  rnmptbd2lem  40036  ssfiunibd  40094  supminfxrrnmpt  40270  climrec  40405  islptre  40421  lptre2pt  40442  limsupmnfuzlem  40528  limsupre3lem  40534  limsupvaluz2  40540  supcnvlimsup  40542  liminfvalxr  40585  ioodvbdlimc1lem2  40717  ioodvbdlimc2lem  40719  stoweidlem27  40813  stoweidlem29  40815  stoweidlem35  40821  stoweidlem48  40834  stoweidlem62  40848  fourierdlem48  40940  fourierdlem64  40956  fourierdlem65  40957  fourierdlem71  40963  fourierdlem73  40965  fourierdlem94  40986  fourierdlem103  40995  fourierdlem104  40996  fourierdlem112  41004  fourierdlem113  41005  sge0isum  41213  sge0seq  41232  meaiuninclem  41266  carageniuncllem2  41308  ovnsslelem  41346  hoidmvlelem1  41381  afvelima  41847  sgoldbeven3prm  42279  nnsum4primes4  42285  nnsum4primesprm  42287  nnsum4primesgbe  42289  nnsum4primesle9  42291  pgrpgt2nabl  42748