Theorem reximdv 3202

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3065

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3070

This theorem is referenced by:  r19.12  3257  r19.12OLD  3258  ss2rexv  3990  reusv3  5328  fvelima  6835  iunpw  7621  frxp  7967  ssfiALT  8957  ordtypelem2  9278  wdom2d  9339  xpwdomg  9344  cff1  10014  iunfo  10295  nqereu  10685  reclem3pr  10805  map2psrpr  10866  supsrlem  10867  1re  10975  elss2prb  14201  exprelprel  14203  o1lo1  15246  rlimcn1  15297  subcn2  15304  lo1add  15336  lo1mul  15337  pythagtriplem19  16534  vdwnnlem2  16697  ramub2  16715  sylow2alem2  19223  lsmless2x  19250  efgrelexlemb  19356  scmateALT  21661  decpmatmulsumfsupp  21922  pmatcollpw1lem1  21923  pmatcollpw2lem  21926  pm2mpmhmlem1  21967  cpmidpmatlem3  22021  cpmidgsum2  22028  tgcl  22119  neiss  22260  ssnei2  22267  tgcnp  22404  cnpco  22418  cnpresti  22439  lmcnp  22455  hausnei2  22504  1stcrest  22604  nlly2i  22627  llyss  22630  nllyss  22631  reftr  22665  lfinun  22676  txcnpi  22759  txcmplem1  22792  tx1stc  22801  nrmr0reg  22900  fbssfi  22988  fbfinnfr  22992  fgcl  23029  ufinffr  23080  elfm2  23099  fmfnfmlem1  23105  fmco  23112  fbflim2  23128  flffbas  23146  flftg  23147  cnpflf2  23151  alexsubALT  23202  cnextcn  23218  isucn2  23431  ucnima  23433  blssexps  23579  blssex  23580  mopni3  23650  neibl  23657  metss  23664  metcnp3  23696  cfilucfil  23715  metustbl  23722  psmetutop  23723  rescncf  24060  lebnum  24127  xlebnum  24128  lebnumii  24129  lmmbr  24422  fgcfil  24435  ovolsslem  24648  ovolunlem1  24661  ovoliunnul  24671  itgcn  25009  ellimc3  25043  c1lip3  25163  itgsubstlem  25212  plyss  25360  ulmclm  25546  ulmcau  25554  ulmcn  25558  rlimcxp  26123  chtppilimlem2  26622  chtppilim  26623  midex  27098  umgrnloop0  27479  usgrnloop0ALT  27572  uhgr2edg  27575  vtxduhgr0nedg  27859  wlkonl1iedg  28033  elwspths2on  28325  3cyclfrgrrn2  28651  isgrpo  28859  tpr2rico  31862  esumpcvgval  32046  omssubadd  32267  connpconn  33197  cvmliftlem15  33260  cvmlift2lem10  33274  satfdmlem  33330  fmla1  33349  satffunlem1lem2  33365  satffunlem2lem2  33368  madess  34059  lrrecfr  34100  fnessref  34546  fvineqsneq  35583  pibt2  35588  ptrecube  35777  poimirlem29  35806  poimirlem30  35807  poimirlem31  35808  fdc1  35904  sstotbnd3  35934  totbndss  35935  heibor1lem  35967  heibor1  35968  opidonOLD  36010  rngmgmbs4  36089  lvoli2  37595  paddss2  37832  lhpexle1lem  38021  lhpexle2lem  38023  dvhdimlem  39458  dvh3dim3N  39463  mapdh9a  39803  hdmap11lem2  39856  sn-negex12  40398  fiphp3d  40641  pell1qrss14  40690  minregex  41141  mnuop3d  41889  grumnudlem  41903  ismnushort  41919  eliuniin  42649  restuni3  42667  eliuniin2  42669  disjrnmpt2  42726  rnmptbd2lem  42794  ssfiunibd  42848  supminfxrrnmpt  43011  climrec  43144  islptre  43160  lptre2pt  43181  limsupmnfuzlem  43267  limsupre3lem  43273  limsupvaluz2  43279  supcnvlimsup  43281  liminfvalxr  43324  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  stoweidlem27  43568  stoweidlem29  43570  stoweidlem35  43576  stoweidlem48  43589  stoweidlem62  43603  fourierdlem48  43695  fourierdlem64  43711  fourierdlem65  43712  fourierdlem71  43718  fourierdlem73  43720  fourierdlem94  43741  fourierdlem103  43750  fourierdlem104  43751  fourierdlem112  43759  fourierdlem113  43760  sge0isum  43965  sge0seq  43984  meaiuninclem  44018  carageniuncllem2  44060  ovnsslelem  44098  hoidmvlelem1  44133  2reuimp  44607  afvelima  44659  sgoldbeven3prm  45235  nnsum4primes4  45241  nnsum4primesprm  45243  nnsum4primesgbe  45245  nnsum4primesle9  45247  pgrpgt2nabl  45702  opnneilv  46202  sepnsepo  46217