Theorem reximdv 3232

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

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

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  r19.12  3283  ss2rexv  3984  reusv3  5271  fvelima  6706  iunpw  7473  frxp  7803  ssfi  8722  ordtypelem2  8967  wdom2d  9028  xpwdomg  9033  cff1  9669  iunfo  9950  nqereu  10340  reclem3pr  10460  map2psrpr  10521  supsrlem  10522  1re  10630  elss2prb  13841  exprelprel  13843  o1lo1  14886  rlimcn1  14937  subcn2  14943  lo1add  14975  lo1mul  14976  pythagtriplem19  16160  vdwnnlem2  16322  ramub2  16340  sylow2alem2  18735  lsmless2x  18762  efgrelexlemb  18868  scmateALT  21117  decpmatmulsumfsupp  21378  pmatcollpw1lem1  21379  pmatcollpw2lem  21382  pm2mpmhmlem1  21423  cpmidpmatlem3  21477  cpmidgsum2  21484  tgcl  21574  neiss  21714  ssnei2  21721  tgcnp  21858  cnpco  21872  cnpresti  21893  lmcnp  21909  hausnei2  21958  1stcrest  22058  nlly2i  22081  llyss  22084  nllyss  22085  reftr  22119  lfinun  22130  txcnpi  22213  txcmplem1  22246  tx1stc  22255  nrmr0reg  22354  fbssfi  22442  fbfinnfr  22446  fgcl  22483  ufinffr  22534  elfm2  22553  fmfnfmlem1  22559  fmco  22566  fbflim2  22582  flffbas  22600  flftg  22601  cnpflf2  22605  alexsubALT  22656  cnextcn  22672  isucn2  22885  ucnima  22887  blssexps  23033  blssex  23034  mopni3  23101  neibl  23108  metss  23115  metcnp3  23147  cfilucfil  23166  metustbl  23173  psmetutop  23174  rescncf  23502  lebnum  23569  xlebnum  23570  lebnumii  23571  lmmbr  23862  fgcfil  23875  ovolsslem  24088  ovolunlem1  24101  ovoliunnul  24111  itgcn  24448  ellimc3  24482  c1lip3  24602  itgsubstlem  24651  plyss  24796  ulmclm  24982  ulmcau  24990  ulmcn  24994  rlimcxp  25559  chtppilimlem2  26058  chtppilim  26059  midex  26531  umgrnloop0  26902  usgrnloop0ALT  26995  uhgr2edg  26998  vtxduhgr0nedg  27282  wlkonl1iedg  27455  elwspths2on  27746  3cyclfrgrrn2  28072  isgrpo  28280  tpr2rico  31265  esumpcvgval  31447  omssubadd  31668  connpconn  32595  cvmliftlem15  32658  cvmlift2lem10  32672  satfdmlem  32728  fmla1  32747  satffunlem1lem2  32763  satffunlem2lem2  32766  fnessref  33818  fvineqsneq  34829  pibt2  34834  ptrecube  35057  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  fdc1  35184  sstotbnd3  35214  totbndss  35215  heibor1lem  35247  heibor1  35248  opidonOLD  35290  rngmgmbs4  35369  lvoli2  36877  paddss2  37114  lhpexle1lem  37303  lhpexle2lem  37305  dvhdimlem  38740  dvh3dim3N  38745  mapdh9a  39085  hdmap11lem2  39138  sn-negex12  39553  fiphp3d  39760  pell1qrss14  39809  mnuop3d  40979  grumnudlem  40993  eliuniin  41735  restuni3  41753  eliuniin2  41755  disjrnmpt2  41815  rnmptbd2lem  41886  ssfiunibd  41941  supminfxrrnmpt  42110  climrec  42245  islptre  42261  lptre2pt  42282  limsupmnfuzlem  42368  limsupre3lem  42374  limsupvaluz2  42380  supcnvlimsup  42382  liminfvalxr  42425  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  stoweidlem27  42669  stoweidlem29  42671  stoweidlem35  42677  stoweidlem48  42690  stoweidlem62  42704  fourierdlem48  42796  fourierdlem64  42812  fourierdlem65  42813  fourierdlem71  42819  fourierdlem73  42821  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem113  42861  sge0isum  43066  sge0seq  43085  meaiuninclem  43119  carageniuncllem2  43161  ovnsslelem  43199  hoidmvlelem1  43234  2reuimp  43671  afvelima  43723  sgoldbeven3prm  44301  nnsum4primes4  44307  nnsum4primesprm  44309  nnsum4primesgbe  44311  nnsum4primesle9  44313  pgrpgt2nabl  44768