Theorem reximdv 3178

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3174	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  r19.12  3312  ss2rexv  4001  reusv3  5367  fvelima  6951  mpt3fvd  7689  iunpw  7786  frxp  8139  nnaordex2  8649  ssfiALT  9190  ordtypelem2  9514  wdom2d  9575  xpwdomg  9580  elhf4  9913  cff1  10337  iunfo  10624  nqereu  11015  reclem3pr  11135  map2psrpr  11196  supsrlem  11197  1re  11309  elss2prb  14634  exprelprel  14636  o1lo1  15705  rlimcn1  15756  subcn2  15763  lo1add  15795  lo1mul  15796  pythagtriplem19  17012  vdwnnlem2  17175  ramub2  17193  mgmidpfod  18858  sylow2alem2  19833  lsmless2x  19860  efgrelexlemb  19965  scmateALT  22828  decpmatmulsumfsupp  23092  pmatcollpw1lem1  23093  pmatcollpw2lem  23096  pm2mpmhmlem1  23137  cpmidpmatlem3  23191  cpmidgsum2  23198  tgcl  23288  neiss  23428  ssnei2  23435  tgcnp  23572  cnpco  23586  cnpresti  23607  lmcnp  23623  hausnei2  23672  1stcrest  23772  nlly2i  23796  llyss  23799  nllyss  23800  reftr  23834  lfinun  23845  txcnpi  23928  txcmplem1  23961  tx1stc  23970  nrmr0reg  24069  fbssfi  24157  fbfinnfr  24161  fgcl  24198  ufinffr  24249  elfm2  24268  fmfnfmlem1  24274  fmco  24281  fbflim2  24297  flffbas  24315  flftg  24316  cnpflf2  24320  alexsubALT  24371  cnextcn  24387  isucn2  24598  ucnima  24600  blssexps  24746  blssex  24747  mopni3  24814  neibl  24821  metss  24828  metcnp3  24860  cfilucfil  24879  metustbl  24886  psmetutop  24887  mpomulcn  25189  rescncf  25219  lebnum  25286  xlebnum  25287  lebnumii  25288  lmmbr  25580  fgcfil  25593  ovolsslem  25806  ovolunlem1  25819  ovoliunnul  25829  itgcn  26166  ellimc3  26200  c1lip3  26320  itgsubstlem  26369  plyss  26518  ulmclm  26715  ulmcau  26723  ulmcn  26727  rlimcxp  27302  chtppilimlem2  27802  chtppilim  27803  madess  28253  lrrecfr  28330  midex  29214  umgrnloop0  29688  usgrnloop0ALT  29787  uhgr2edg  29790  vtxduhgr0nedg  30074  wlkonl1iedg  30245  elwspths2on  30552  elwspths2onw  30553  3cyclfrgrrn2  30889  isgrpo  31100  tpr2rico  34545  esumpcvgval  34711  omssubadd  34933  r1filim  35730  fineqvnttrclse  35793  vonf1oonfo  35899  connpconn  36001  cvmliftlem15  36064  cvmlift2lem10  36078  satfdmlem  36134  fmla1  36153  satffunlem1lem2  36169  satffunlem2lem2  36172  fnessref  37146  ttctr  37282  fvineqsneq  38337  pibt2  38342  ptrecube  38540  poimirlem29  38569  poimirlem30  38570  poimirlem31  38571  dfprop2  38648  fdc1  38682  sstotbnd3  38712  totbndss  38713  heibor1lem  38745  heibor1  38746  opidonOLD  38788  rngmgmbs4  38867  lvoli2  40640  paddss2  40877  lhpexle1lem  41066  lhpexle2lem  41068  dvhdimlem  42503  dvh3dim3N  42508  mapdh9a  42848  hdmap11lem2  42901  fiphp3d  43827  pell1qrss14  43876  minregex  44536  mnuop3d  45256  grumnudlem  45270  ismnushort  45286  eliuniin  46115  restuni3  46134  eliuniin2  46136  disjrnmpt2  46204  rnmptbd2lem  46261  ssfiunibd  46326  supminfxrrnmpt  46482  climrec  46616  islptre  46632  lptre2pt  46651  limsupmnfuzlem  46737  limsupre3lem  46743  limsupvaluz2  46749  supcnvlimsup  46751  liminfvalxr  46794  ioodvbdlimc1lem2  46943  ioodvbdlimc2lem  46945  stoweidlem27  47038  stoweidlem29  47040  stoweidlem35  47046  stoweidlem48  47059  stoweidlem62  47073  fourierdlem48  47165  fourierdlem64  47181  fourierdlem65  47182  fourierdlem71  47188  fourierdlem73  47190  fourierdlem94  47211  fourierdlem103  47220  fourierdlem104  47221  fourierdlem112  47229  fourierdlem113  47230  sge0isum  47438  sge0seq  47457  meaiuninclem  47491  carageniuncllem2  47533  ovnsslelem  47571  hoidmvlelem1  47606  2reuimp  48186  afvelima  48238  sgoldbeven3prm  48882  nnsum4primes4  48888  nnsum4primesprm  48890  nnsum4primesgbe  48892  nnsum4primesle9  48894  grtriprop  49040  pgrpgt2nabl  49479  opnneilv  50018  sepnsepo  50033