Theorem reximdv 3176

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  r19.12  3310  ss2rexv  4006  reusv3  5359  fvelima  6926  iunpw  7748  frxp  8099  nnaordex2  8602  ssfiALT  9135  ordtypelem2  9460  wdom2d  9521  xpwdomg  9526  cff1  10208  iunfo  10489  nqereu  10880  reclem3pr  11000  map2psrpr  11061  supsrlem  11062  1re  11174  elss2prb  14494  exprelprel  14496  o1lo1  15554  rlimcn1  15605  subcn2  15612  lo1add  15644  lo1mul  15645  pythagtriplem19  16859  vdwnnlem2  17022  ramub2  17040  sylow2alem2  19648  lsmless2x  19675  efgrelexlemb  19780  scmateALT  22559  decpmatmulsumfsupp  22820  pmatcollpw1lem1  22821  pmatcollpw2lem  22824  pm2mpmhmlem1  22865  cpmidpmatlem3  22919  cpmidgsum2  22926  tgcl  23016  neiss  23156  ssnei2  23163  tgcnp  23300  cnpco  23314  cnpresti  23335  lmcnp  23351  hausnei2  23400  1stcrest  23500  nlly2i  23523  llyss  23526  nllyss  23527  reftr  23561  lfinun  23572  txcnpi  23655  txcmplem1  23688  tx1stc  23697  nrmr0reg  23796  fbssfi  23884  fbfinnfr  23888  fgcl  23925  ufinffr  23976  elfm2  23995  fmfnfmlem1  24001  fmco  24008  fbflim2  24024  flffbas  24042  flftg  24043  cnpflf2  24047  alexsubALT  24098  cnextcn  24114  isucn2  24325  ucnima  24327  blssexps  24473  blssex  24474  mopni3  24541  neibl  24548  metss  24555  metcnp3  24587  cfilucfil  24606  metustbl  24613  psmetutop  24614  mpomulcn  24916  rescncf  24946  lebnum  25013  xlebnum  25014  lebnumii  25015  lmmbr  25307  fgcfil  25320  ovolsslem  25533  ovolunlem1  25546  ovoliunnul  25556  itgcn  25894  ellimc3  25928  c1lip3  26048  itgsubstlem  26097  plyss  26246  ulmclm  26437  ulmcau  26445  ulmcn  26449  rlimcxp  27025  chtppilimlem2  27525  chtppilim  27526  madess  27946  lrrecfr  28023  midex  28893  umgrnloop0  29266  usgrnloop0ALT  29362  uhgr2edg  29365  vtxduhgr0nedg  29649  wlkonl1iedg  29820  elwspths2on  30118  elwspths2onw  30119  3cyclfrgrrn2  30445  isgrpo  30656  tpr2rico  34169  esumpcvgval  34335  omssubadd  34557  r1filim  35360  fineqvnttrclse  35380  vonf1oonfo  35418  connpconn  35545  cvmliftlem15  35608  cvmlift2lem10  35622  satfdmlem  35678  fmla1  35697  satffunlem1lem2  35713  satffunlem2lem2  35716  fnessref  36677  ttctr  36813  fvineqsneq  37866  pibt2  37871  ptrecube  38079  poimirlem29  38108  poimirlem30  38109  poimirlem31  38110  fdc1  38205  sstotbnd3  38235  totbndss  38236  heibor1lem  38268  heibor1  38269  opidonOLD  38311  rngmgmbs4  38390  lvoli2  40165  paddss2  40402  lhpexle1lem  40591  lhpexle2lem  40593  dvhdimlem  42028  dvh3dim3N  42033  mapdh9a  42373  hdmap11lem2  42426  fiphp3d  43356  pell1qrss14  43405  minregex  44070  mnuop3d  44807  grumnudlem  44821  ismnushort  44837  eliuniin  45637  restuni3  45656  eliuniin2  45658  disjrnmpt2  45726  rnmptbd2lem  45783  ssfiunibd  45848  supminfxrrnmpt  46005  climrec  46139  islptre  46155  lptre2pt  46174  limsupmnfuzlem  46260  limsupre3lem  46266  limsupvaluz2  46272  supcnvlimsup  46274  liminfvalxr  46317  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  stoweidlem27  46561  stoweidlem29  46563  stoweidlem35  46569  stoweidlem48  46582  stoweidlem62  46596  fourierdlem48  46688  fourierdlem64  46704  fourierdlem65  46705  fourierdlem71  46711  fourierdlem73  46713  fourierdlem94  46734  fourierdlem103  46743  fourierdlem104  46744  fourierdlem112  46752  fourierdlem113  46753  sge0isum  46961  sge0seq  46980  meaiuninclem  47014  carageniuncllem2  47056  ovnsslelem  47094  hoidmvlelem1  47129  2reuimp  47669  afvelima  47721  sgoldbeven3prm  48365  nnsum4primes4  48371  nnsum4primesprm  48373  nnsum4primesgbe  48375  nnsum4primesle9  48377  grtriprop  48523  pgrpgt2nabl  48948  opnneilv  49490  sepnsepo  49505