Theorem reximdv 3149

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054

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 3055

This theorem is referenced by:  r19.12  3290  ss2rexv  4021  reusv3  5363  fvelima  6929  iunpw  7750  frxp  8108  nnaordex2  8606  ssfiALT  9144  ordtypelem2  9479  wdom2d  9540  xpwdomg  9545  cff1  10218  iunfo  10499  nqereu  10889  reclem3pr  11009  map2psrpr  11070  supsrlem  11071  1re  11181  elss2prb  14460  exprelprel  14462  o1lo1  15510  rlimcn1  15561  subcn2  15568  lo1add  15600  lo1mul  15601  pythagtriplem19  16811  vdwnnlem2  16974  ramub2  16992  sylow2alem2  19555  lsmless2x  19582  efgrelexlemb  19687  scmateALT  22406  decpmatmulsumfsupp  22667  pmatcollpw1lem1  22668  pmatcollpw2lem  22671  pm2mpmhmlem1  22712  cpmidpmatlem3  22766  cpmidgsum2  22773  tgcl  22863  neiss  23003  ssnei2  23010  tgcnp  23147  cnpco  23161  cnpresti  23182  lmcnp  23198  hausnei2  23247  1stcrest  23347  nlly2i  23370  llyss  23373  nllyss  23374  reftr  23408  lfinun  23419  txcnpi  23502  txcmplem1  23535  tx1stc  23544  nrmr0reg  23643  fbssfi  23731  fbfinnfr  23735  fgcl  23772  ufinffr  23823  elfm2  23842  fmfnfmlem1  23848  fmco  23855  fbflim2  23871  flffbas  23889  flftg  23890  cnpflf2  23894  alexsubALT  23945  cnextcn  23961  isucn2  24173  ucnima  24175  blssexps  24321  blssex  24322  mopni3  24389  neibl  24396  metss  24403  metcnp3  24435  cfilucfil  24454  metustbl  24461  psmetutop  24462  mpomulcn  24765  rescncf  24797  lebnum  24870  xlebnum  24871  lebnumii  24872  lmmbr  25165  fgcfil  25178  ovolsslem  25392  ovolunlem1  25405  ovoliunnul  25415  itgcn  25753  ellimc3  25787  c1lip3  25911  itgsubstlem  25962  plyss  26111  ulmclm  26303  ulmcau  26311  ulmcn  26315  rlimcxp  26891  chtppilimlem2  27392  chtppilim  27393  madess  27795  lrrecfr  27857  midex  28671  umgrnloop0  29043  usgrnloop0ALT  29139  uhgr2edg  29142  vtxduhgr0nedg  29427  wlkonl1iedg  29600  elwspths2on  29897  3cyclfrgrrn2  30223  isgrpo  30433  tpr2rico  33909  esumpcvgval  34075  omssubadd  34298  connpconn  35229  cvmliftlem15  35292  cvmlift2lem10  35306  satfdmlem  35362  fmla1  35381  satffunlem1lem2  35397  satffunlem2lem2  35400  fnessref  36352  fvineqsneq  37407  pibt2  37412  ptrecube  37621  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  fdc1  37747  sstotbnd3  37777  totbndss  37778  heibor1lem  37810  heibor1  37811  opidonOLD  37853  rngmgmbs4  37932  lvoli2  39582  paddss2  39819  lhpexle1lem  40008  lhpexle2lem  40010  dvhdimlem  41445  dvh3dim3N  41450  mapdh9a  41790  hdmap11lem2  41843  fiphp3d  42814  pell1qrss14  42863  minregex  43530  mnuop3d  44267  grumnudlem  44281  ismnushort  44297  eliuniin  45100  restuni3  45119  eliuniin2  45121  disjrnmpt2  45189  rnmptbd2lem  45249  ssfiunibd  45314  supminfxrrnmpt  45474  climrec  45608  islptre  45624  lptre2pt  45645  limsupmnfuzlem  45731  limsupre3lem  45737  limsupvaluz2  45743  supcnvlimsup  45745  liminfvalxr  45788  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem27  46032  stoweidlem29  46034  stoweidlem35  46040  stoweidlem48  46053  stoweidlem62  46067  fourierdlem48  46159  fourierdlem64  46175  fourierdlem65  46176  fourierdlem71  46182  fourierdlem73  46184  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  sge0isum  46432  sge0seq  46451  meaiuninclem  46485  carageniuncllem2  46527  ovnsslelem  46565  hoidmvlelem1  46600  2reuimp  47120  afvelima  47172  sgoldbeven3prm  47788  nnsum4primes4  47794  nnsum4primesprm  47796  nnsum4primesgbe  47798  nnsum4primesle9  47800  grtriprop  47944  pgrpgt2nabl  48358  opnneilv  48901  sepnsepo  48916