Theorem reximdv 3224

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

Syntax hints:   → wi 4   ∈ wcel 2164  ∃wrex 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-ral 3122  df-rex 3123

This theorem is referenced by:  r19.12  3273  reusv3  5105  fvelima  6495  iunpw  7239  frxp  7551  ssfi  8449  ordtypelem2  8693  wdom2d  8754  xpwdomg  8759  cff1  9395  iunfo  9676  nqereu  10066  reclem3pr  10186  map2psrpr  10247  supsrlem  10248  1re  10356  elss2prb  13558  exprelprel  13560  o1lo1  14645  rlimcn1  14696  subcn2  14702  lo1add  14734  lo1mul  14735  pythagtriplem19  15909  vdwnnlem2  16071  ramub2  16089  sylow2alem2  18384  lsmless2x  18411  efgrelexlemb  18516  scmateALT  20686  decpmatmulsumfsupp  20948  pmatcollpw1lem1  20949  pmatcollpw2lem  20952  pm2mpmhmlem1  20993  cpmidpmatlem3  21047  cpmidgsum2  21054  tgcl  21144  neiss  21284  ssnei2  21291  tgcnp  21428  cnpco  21442  cnpresti  21463  lmcnp  21479  hausnei2  21528  1stcrest  21627  nlly2i  21650  llyss  21653  nllyss  21654  reftr  21688  lfinun  21699  txcnpi  21782  txcmplem1  21815  tx1stc  21824  nrmr0reg  21923  fbssfi  22011  fbfinnfr  22015  fgcl  22052  ufinffr  22103  elfm2  22122  fmfnfmlem1  22128  fmco  22135  fbflim2  22151  flffbas  22169  flftg  22170  cnpflf2  22174  alexsubALT  22225  cnextcn  22241  isucn2  22453  ucnima  22455  blssexps  22601  blssex  22602  mopni3  22669  neibl  22676  metss  22683  metcnp3  22715  cfilucfil  22734  metustbl  22741  psmetutop  22742  rescncf  23070  lebnum  23133  xlebnum  23134  lebnumii  23135  lmmbr  23426  fgcfil  23439  ovolsslem  23650  ovolunlem1  23663  ovoliunnul  23673  itgcn  24008  ellimc3  24042  c1lip3  24161  itgsubstlem  24210  plyss  24354  ulmclm  24540  ulmcau  24548  ulmcn  24552  rlimcxp  25113  chtppilimlem2  25576  chtppilim  25577  midex  26046  umgrnloop0  26407  usgrnloop0ALT  26501  uhgr2edg  26504  vtxduhgr0nedg  26790  wlkonl1iedg  26962  elwspths2on  27289  3cyclfrgrrn2  27657  isgrpo  27896  tpr2rico  30492  esumpcvgval  30674  omssubadd  30896  connpconn  31752  cvmliftlem15  31815  cvmlift2lem10  31829  fnessref  32879  ptrecube  33946  poimirlem29  33975  poimirlem30  33976  poimirlem31  33977  fdc1  34077  sstotbnd3  34110  totbndss  34111  heibor1lem  34143  heibor1  34144  opidonOLD  34186  rngmgmbs4  34265  lvoli2  35649  paddss2  35886  lhpexle1lem  36075  lhpexle2lem  36077  dvhdimlem  37512  dvh3dim3N  37517  mapdh9a  37857  hdmap11lem2  37910  fiphp3d  38220  pell1qrss14  38269  eliuniin  40089  restuni3  40109  eliuniin2  40111  disjrnmpt2  40176  rnmptbd2lem  40256  ssfiunibd  40314  supminfxrrnmpt  40488  climrec  40623  islptre  40639  lptre2pt  40660  limsupmnfuzlem  40746  limsupre3lem  40752  limsupvaluz2  40758  supcnvlimsup  40760  liminfvalxr  40803  ioodvbdlimc1lem2  40935  ioodvbdlimc2lem  40937  stoweidlem27  41031  stoweidlem29  41033  stoweidlem35  41039  stoweidlem48  41052  stoweidlem62  41066  fourierdlem48  41158  fourierdlem64  41174  fourierdlem65  41175  fourierdlem71  41181  fourierdlem73  41183  fourierdlem94  41204  fourierdlem103  41213  fourierdlem104  41214  fourierdlem112  41222  fourierdlem113  41223  sge0isum  41428  sge0seq  41447  meaiuninclem  41481  carageniuncllem2  41523  ovnsslelem  41561  hoidmvlelem1  41596  afvelima  42062  sgoldbeven3prm  42494  nnsum4primes4  42500  nnsum4primesprm  42502  nnsum4primesgbe  42504  nnsum4primesle9  42506  pgrpgt2nabl  42987