Theorem reximdv 3016

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  r19.12  3063  reusv3  4876  fvelima  6248  iunpw  6978  frxp  7287  ssfi  8180  ordtypelem2  8424  wdom2d  8485  xpwdomg  8490  cff1  9080  iunfo  9361  nqereu  9751  reclem3pr  9871  map2psrpr  9931  supsrlem  9932  1re  10039  elss2prb  13269  exprelprel  13271  o1lo1  14268  rlimcn1  14319  subcn2  14325  lo1add  14357  lo1mul  14358  pythagtriplem19  15538  vdwnnlem2  15700  ramub2  15718  sylow2alem2  18033  lsmless2x  18060  efgrelexlemb  18163  scmateALT  20318  decpmatmulsumfsupp  20578  pmatcollpw1lem1  20579  pmatcollpw2lem  20582  pm2mpmhmlem1  20623  cpmidpmatlem3  20677  cpmidgsum2  20684  tgcl  20773  neiss  20913  ssnei2  20920  tgcnp  21057  cnpco  21071  cnpresti  21092  lmcnp  21108  hausnei2  21157  1stcrest  21256  nlly2i  21279  llyss  21282  nllyss  21283  reftr  21317  lfinun  21328  txcnpi  21411  txcmplem1  21444  tx1stc  21453  nrmr0reg  21552  fbssfi  21641  fbfinnfr  21645  fgcl  21682  ufinffr  21733  elfm2  21752  fmfnfmlem1  21758  fmco  21765  fbflim2  21781  flffbas  21799  flftg  21800  cnpflf2  21804  alexsubALT  21855  cnextcn  21871  isucn2  22083  ucnima  22085  blssexps  22231  blssex  22232  mopni3  22299  neibl  22306  metss  22313  metcnp3  22345  cfilucfil  22364  metustbl  22371  psmetutop  22372  rescncf  22700  lebnum  22763  xlebnum  22764  lebnumii  22765  lmmbr  23056  fgcfil  23069  ovolsslem  23252  ovolunlem1  23265  ovoliunnul  23275  itgcn  23609  ellimc3  23643  c1lip3  23762  itgsubstlem  23811  plyss  23955  ulmclm  24141  ulmcau  24149  ulmcn  24153  rlimcxp  24700  chtppilimlem2  25163  chtppilim  25164  midex  25629  umgrnloop0  26004  usgrnloop0ALT  26097  uhgr2edg  26100  vtxduhgr0nedg  26388  wlkonl1iedg  26561  elwspths2on  26853  3cyclfrgrrn2  27151  isgrpo  27351  tpr2rico  29958  esumpcvgval  30140  omssubadd  30362  connpconn  31217  cvmliftlem15  31280  cvmlift2lem10  31294  fnessref  32352  ptrecube  33409  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  fdc1  33542  sstotbnd3  33575  totbndss  33576  heibor1lem  33608  heibor1  33609  opidonOLD  33651  rngmgmbs4  33730  lvoli2  34867  paddss2  35104  lhpexle1lem  35293  lhpexle2lem  35295  dvhdimlem  36733  dvh3dim3N  36738  mapdh9a  37079  hdmap11lem2  37134  fiphp3d  37383  pell1qrss14  37432  eliuniin  39279  restuni3  39301  eliuniin2  39303  disjrnmpt2  39375  rnmptbd2lem  39463  ssfiunibd  39523  supminfxrrnmpt  39701  climrec  39835  islptre  39851  lptre2pt  39872  limsupmnfuzlem  39958  limsupre3lem  39964  limsupvaluz2  39970  supcnvlimsup  39972  liminfvalxr  40015  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem27  40244  stoweidlem29  40246  stoweidlem35  40252  stoweidlem48  40265  stoweidlem62  40279  fourierdlem48  40371  fourierdlem64  40387  fourierdlem65  40388  fourierdlem71  40394  fourierdlem73  40396  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  sge0isum  40644  sge0seq  40663  meaiuninclem  40697  carageniuncllem2  40736  ovnsslelem  40774  hoidmvlelem1  40809  afvelima  41247  sgoldbeven3prm  41671  nnsum4primes4  41677  nnsum4primesprm  41679  nnsum4primesgbe  41681  nnsum4primesle9  41683  pgrpgt2nabl  42147