Theorem reximdv 3147

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  r19.12  3281  ss2rexv  4001  reusv3  5338  fvelima  6882  iunpw  7699  frxp  8051  nnaordex2  8549  ssfiALT  9078  ordtypelem2  9400  wdom2d  9461  xpwdomg  9466  cff1  10144  iunfo  10425  nqereu  10815  reclem3pr  10935  map2psrpr  10996  supsrlem  10997  1re  11107  elss2prb  14390  exprelprel  14392  o1lo1  15439  rlimcn1  15490  subcn2  15497  lo1add  15529  lo1mul  15530  pythagtriplem19  16740  vdwnnlem2  16903  ramub2  16921  sylow2alem2  19525  lsmless2x  19552  efgrelexlemb  19657  scmateALT  22422  decpmatmulsumfsupp  22683  pmatcollpw1lem1  22684  pmatcollpw2lem  22687  pm2mpmhmlem1  22728  cpmidpmatlem3  22782  cpmidgsum2  22789  tgcl  22879  neiss  23019  ssnei2  23026  tgcnp  23163  cnpco  23177  cnpresti  23198  lmcnp  23214  hausnei2  23263  1stcrest  23363  nlly2i  23386  llyss  23389  nllyss  23390  reftr  23424  lfinun  23435  txcnpi  23518  txcmplem1  23551  tx1stc  23560  nrmr0reg  23659  fbssfi  23747  fbfinnfr  23751  fgcl  23788  ufinffr  23839  elfm2  23858  fmfnfmlem1  23864  fmco  23871  fbflim2  23887  flffbas  23905  flftg  23906  cnpflf2  23910  alexsubALT  23961  cnextcn  23977  isucn2  24188  ucnima  24190  blssexps  24336  blssex  24337  mopni3  24404  neibl  24411  metss  24418  metcnp3  24450  cfilucfil  24469  metustbl  24476  psmetutop  24477  mpomulcn  24780  rescncf  24812  lebnum  24885  xlebnum  24886  lebnumii  24887  lmmbr  25180  fgcfil  25193  ovolsslem  25407  ovolunlem1  25420  ovoliunnul  25430  itgcn  25768  ellimc3  25802  c1lip3  25926  itgsubstlem  25977  plyss  26126  ulmclm  26318  ulmcau  26326  ulmcn  26330  rlimcxp  26906  chtppilimlem2  27407  chtppilim  27408  madess  27816  lrrecfr  27881  midex  28710  umgrnloop0  29082  usgrnloop0ALT  29178  uhgr2edg  29181  vtxduhgr0nedg  29466  wlkonl1iedg  29637  elwspths2on  29933  3cyclfrgrrn2  30259  isgrpo  30469  tpr2rico  33917  esumpcvgval  34083  omssubadd  34305  r1filim  35107  fineqvnttrclse  35136  connpconn  35271  cvmliftlem15  35334  cvmlift2lem10  35348  satfdmlem  35404  fmla1  35423  satffunlem1lem2  35439  satffunlem2lem2  35442  fnessref  36391  fvineqsneq  37446  pibt2  37451  ptrecube  37660  poimirlem29  37689  poimirlem30  37690  poimirlem31  37691  fdc1  37786  sstotbnd3  37816  totbndss  37817  heibor1lem  37849  heibor1  37850  opidonOLD  37892  rngmgmbs4  37971  lvoli2  39620  paddss2  39857  lhpexle1lem  40046  lhpexle2lem  40048  dvhdimlem  41483  dvh3dim3N  41488  mapdh9a  41828  hdmap11lem2  41881  fiphp3d  42852  pell1qrss14  42901  minregex  43567  mnuop3d  44304  grumnudlem  44318  ismnushort  44334  eliuniin  45136  restuni3  45155  eliuniin2  45157  disjrnmpt2  45225  rnmptbd2lem  45285  ssfiunibd  45350  supminfxrrnmpt  45509  climrec  45643  islptre  45659  lptre2pt  45678  limsupmnfuzlem  45764  limsupre3lem  45770  limsupvaluz2  45776  supcnvlimsup  45778  liminfvalxr  45821  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  stoweidlem27  46065  stoweidlem29  46067  stoweidlem35  46073  stoweidlem48  46086  stoweidlem62  46100  fourierdlem48  46192  fourierdlem64  46208  fourierdlem65  46209  fourierdlem71  46215  fourierdlem73  46217  fourierdlem94  46238  fourierdlem103  46247  fourierdlem104  46248  fourierdlem112  46256  fourierdlem113  46257  sge0isum  46465  sge0seq  46484  meaiuninclem  46518  carageniuncllem2  46560  ovnsslelem  46598  hoidmvlelem1  46633  2reuimp  47146  afvelima  47198  sgoldbeven3prm  47814  nnsum4primes4  47820  nnsum4primesprm  47822  nnsum4primesgbe  47824  nnsum4primesle9  47826  grtriprop  47972  pgrpgt2nabl  48397  opnneilv  48940  sepnsepo  48955