Theorem reximdv 3155

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3060

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 3061

This theorem is referenced by:  r19.12  3294  ss2rexv  4030  reusv3  5375  fvelima  6943  iunpw  7763  frxp  8123  nnaordex2  8649  ssfiALT  9186  ordtypelem2  9531  wdom2d  9592  xpwdomg  9597  cff1  10270  iunfo  10551  nqereu  10941  reclem3pr  11061  map2psrpr  11122  supsrlem  11123  1re  11233  elss2prb  14504  exprelprel  14506  o1lo1  15551  rlimcn1  15602  subcn2  15609  lo1add  15641  lo1mul  15642  pythagtriplem19  16851  vdwnnlem2  17014  ramub2  17032  sylow2alem2  19597  lsmless2x  19624  efgrelexlemb  19729  scmateALT  22448  decpmatmulsumfsupp  22709  pmatcollpw1lem1  22710  pmatcollpw2lem  22713  pm2mpmhmlem1  22754  cpmidpmatlem3  22808  cpmidgsum2  22815  tgcl  22905  neiss  23045  ssnei2  23052  tgcnp  23189  cnpco  23203  cnpresti  23224  lmcnp  23240  hausnei2  23289  1stcrest  23389  nlly2i  23412  llyss  23415  nllyss  23416  reftr  23450  lfinun  23461  txcnpi  23544  txcmplem1  23577  tx1stc  23586  nrmr0reg  23685  fbssfi  23773  fbfinnfr  23777  fgcl  23814  ufinffr  23865  elfm2  23884  fmfnfmlem1  23890  fmco  23897  fbflim2  23913  flffbas  23931  flftg  23932  cnpflf2  23936  alexsubALT  23987  cnextcn  24003  isucn2  24215  ucnima  24217  blssexps  24363  blssex  24364  mopni3  24431  neibl  24438  metss  24445  metcnp3  24477  cfilucfil  24496  metustbl  24503  psmetutop  24504  mpomulcn  24807  rescncf  24839  lebnum  24912  xlebnum  24913  lebnumii  24914  lmmbr  25208  fgcfil  25221  ovolsslem  25435  ovolunlem1  25448  ovoliunnul  25458  itgcn  25796  ellimc3  25830  c1lip3  25954  itgsubstlem  26005  plyss  26154  ulmclm  26346  ulmcau  26354  ulmcn  26358  rlimcxp  26934  chtppilimlem2  27435  chtppilim  27436  madess  27832  lrrecfr  27893  midex  28662  umgrnloop0  29034  usgrnloop0ALT  29130  uhgr2edg  29133  vtxduhgr0nedg  29418  wlkonl1iedg  29591  elwspths2on  29888  3cyclfrgrrn2  30214  isgrpo  30424  tpr2rico  33889  esumpcvgval  34055  omssubadd  34278  connpconn  35203  cvmliftlem15  35266  cvmlift2lem10  35280  satfdmlem  35336  fmla1  35355  satffunlem1lem2  35371  satffunlem2lem2  35374  fnessref  36321  fvineqsneq  37376  pibt2  37381  ptrecube  37590  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  fdc1  37716  sstotbnd3  37746  totbndss  37747  heibor1lem  37779  heibor1  37780  opidonOLD  37822  rngmgmbs4  37901  lvoli2  39546  paddss2  39783  lhpexle1lem  39972  lhpexle2lem  39974  dvhdimlem  41409  dvh3dim3N  41414  mapdh9a  41754  hdmap11lem2  41807  fiphp3d  42789  pell1qrss14  42838  minregex  43505  mnuop3d  44243  grumnudlem  44257  ismnushort  44273  eliuniin  45071  restuni3  45090  eliuniin2  45092  disjrnmpt2  45160  rnmptbd2lem  45220  ssfiunibd  45286  supminfxrrnmpt  45446  climrec  45580  islptre  45596  lptre2pt  45617  limsupmnfuzlem  45703  limsupre3lem  45709  limsupvaluz2  45715  supcnvlimsup  45717  liminfvalxr  45760  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  stoweidlem27  46004  stoweidlem29  46006  stoweidlem35  46012  stoweidlem48  46025  stoweidlem62  46039  fourierdlem48  46131  fourierdlem64  46147  fourierdlem65  46148  fourierdlem71  46154  fourierdlem73  46156  fourierdlem94  46177  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  fourierdlem113  46196  sge0isum  46404  sge0seq  46423  meaiuninclem  46457  carageniuncllem2  46499  ovnsslelem  46537  hoidmvlelem1  46572  2reuimp  47092  afvelima  47144  sgoldbeven3prm  47745  nnsum4primes4  47751  nnsum4primesprm  47753  nnsum4primesgbe  47755  nnsum4primesle9  47757  grtriprop  47901  pgrpgt2nabl  48289  opnneilv  48831  sepnsepo  48846