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  4003  reusv3  5367  fvelima  6948  mpt3fvd  7686  iunpw  7783  frxp  8136  nnaordex2  8641  ssfiALT  9182  ordtypelem2  9506  wdom2d  9567  xpwdomg  9572  elhf4  9905  cff1  10329  iunfo  10616  nqereu  11007  reclem3pr  11127  map2psrpr  11188  supsrlem  11189  1re  11301  elss2prb  14626  exprelprel  14628  o1lo1  15697  rlimcn1  15748  subcn2  15755  lo1add  15787  lo1mul  15788  pythagtriplem19  17004  vdwnnlem2  17167  ramub2  17185  mgmidpfod  18850  sylow2alem2  19825  lsmless2x  19852  efgrelexlemb  19957  scmateALT  22820  decpmatmulsumfsupp  23084  pmatcollpw1lem1  23085  pmatcollpw2lem  23088  pm2mpmhmlem1  23129  cpmidpmatlem3  23183  cpmidgsum2  23190  tgcl  23280  neiss  23420  ssnei2  23427  tgcnp  23564  cnpco  23578  cnpresti  23599  lmcnp  23615  hausnei2  23664  1stcrest  23764  nlly2i  23788  llyss  23791  nllyss  23792  reftr  23826  lfinun  23837  txcnpi  23920  txcmplem1  23953  tx1stc  23962  nrmr0reg  24061  fbssfi  24149  fbfinnfr  24153  fgcl  24190  ufinffr  24241  elfm2  24260  fmfnfmlem1  24266  fmco  24273  fbflim2  24289  flffbas  24307  flftg  24308  cnpflf2  24312  alexsubALT  24363  cnextcn  24379  isucn2  24590  ucnima  24592  blssexps  24738  blssex  24739  mopni3  24806  neibl  24813  metss  24820  metcnp3  24852  cfilucfil  24871  metustbl  24878  psmetutop  24879  mpomulcn  25181  rescncf  25211  lebnum  25278  xlebnum  25279  lebnumii  25280  lmmbr  25572  fgcfil  25585  ovolsslem  25798  ovolunlem1  25811  ovoliunnul  25821  itgcn  26158  ellimc3  26192  c1lip3  26312  itgsubstlem  26361  plyss  26510  ulmclm  26707  ulmcau  26715  ulmcn  26719  rlimcxp  27294  chtppilimlem2  27794  chtppilim  27795  madess  28245  lrrecfr  28322  midex  29206  umgrnloop0  29680  usgrnloop0ALT  29779  uhgr2edg  29782  vtxduhgr0nedg  30066  wlkonl1iedg  30237  elwspths2on  30544  elwspths2onw  30545  3cyclfrgrrn2  30881  isgrpo  31092  tpr2rico  34537  esumpcvgval  34703  omssubadd  34925  r1filim  35718  fineqvnttrclse  35775  vonf1oonfo  35877  connpconn  35979  cvmliftlem15  36042  cvmlift2lem10  36056  satfdmlem  36112  fmla1  36131  satffunlem1lem2  36147  satffunlem2lem2  36150  fnessref  37125  ttctr  37261  fvineqsneq  38315  pibt2  38320  ptrecube  38518  poimirlem29  38547  poimirlem30  38548  poimirlem31  38549  dfprop2  38626  fdc1  38660  sstotbnd3  38690  totbndss  38691  heibor1lem  38723  heibor1  38724  opidonOLD  38766  rngmgmbs4  38845  lvoli2  40618  paddss2  40855  lhpexle1lem  41044  lhpexle2lem  41046  dvhdimlem  42481  dvh3dim3N  42486  mapdh9a  42826  hdmap11lem2  42879  fiphp3d  43805  pell1qrss14  43854  minregex  44519  mnuop3d  45240  grumnudlem  45254  ismnushort  45270  eliuniin  46083  restuni3  46102  eliuniin2  46104  disjrnmpt2  46172  rnmptbd2lem  46229  ssfiunibd  46294  supminfxrrnmpt  46450  climrec  46584  islptre  46600  lptre2pt  46619  limsupmnfuzlem  46705  limsupre3lem  46711  limsupvaluz2  46717  supcnvlimsup  46719  liminfvalxr  46762  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  stoweidlem27  47006  stoweidlem29  47008  stoweidlem35  47014  stoweidlem48  47027  stoweidlem62  47041  fourierdlem48  47133  fourierdlem64  47149  fourierdlem65  47150  fourierdlem71  47156  fourierdlem73  47158  fourierdlem94  47179  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  fourierdlem113  47198  sge0isum  47406  sge0seq  47425  meaiuninclem  47459  carageniuncllem2  47501  ovnsslelem  47539  hoidmvlelem1  47574  2reuimp  48154  afvelima  48206  sgoldbeven3prm  48850  nnsum4primes4  48856  nnsum4primesprm  48858  nnsum4primesgbe  48860  nnsum4primesle9  48862  grtriprop  49008  pgrpgt2nabl  49447  opnneilv  49986  sepnsepo  50001