Theorem reximdv 3144

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.12  3279  ss2rexv  4009  reusv3  5347  fvelima  6892  iunpw  7711  frxp  8066  nnaordex2  8564  ssfiALT  9098  ordtypelem2  9430  wdom2d  9491  xpwdomg  9496  cff1  10171  iunfo  10452  nqereu  10842  reclem3pr  10962  map2psrpr  11023  supsrlem  11024  1re  11134  elss2prb  14413  exprelprel  14415  o1lo1  15462  rlimcn1  15513  subcn2  15520  lo1add  15552  lo1mul  15553  pythagtriplem19  16763  vdwnnlem2  16926  ramub2  16944  sylow2alem2  19515  lsmless2x  19542  efgrelexlemb  19647  scmateALT  22415  decpmatmulsumfsupp  22676  pmatcollpw1lem1  22677  pmatcollpw2lem  22680  pm2mpmhmlem1  22721  cpmidpmatlem3  22775  cpmidgsum2  22782  tgcl  22872  neiss  23012  ssnei2  23019  tgcnp  23156  cnpco  23170  cnpresti  23191  lmcnp  23207  hausnei2  23256  1stcrest  23356  nlly2i  23379  llyss  23382  nllyss  23383  reftr  23417  lfinun  23428  txcnpi  23511  txcmplem1  23544  tx1stc  23553  nrmr0reg  23652  fbssfi  23740  fbfinnfr  23744  fgcl  23781  ufinffr  23832  elfm2  23851  fmfnfmlem1  23857  fmco  23864  fbflim2  23880  flffbas  23898  flftg  23899  cnpflf2  23903  alexsubALT  23954  cnextcn  23970  isucn2  24182  ucnima  24184  blssexps  24330  blssex  24331  mopni3  24398  neibl  24405  metss  24412  metcnp3  24444  cfilucfil  24463  metustbl  24470  psmetutop  24471  mpomulcn  24774  rescncf  24806  lebnum  24879  xlebnum  24880  lebnumii  24881  lmmbr  25174  fgcfil  25187  ovolsslem  25401  ovolunlem1  25414  ovoliunnul  25424  itgcn  25762  ellimc3  25796  c1lip3  25920  itgsubstlem  25971  plyss  26120  ulmclm  26312  ulmcau  26320  ulmcn  26324  rlimcxp  26900  chtppilimlem2  27401  chtppilim  27402  madess  27808  lrrecfr  27873  midex  28700  umgrnloop0  29072  usgrnloop0ALT  29168  uhgr2edg  29171  vtxduhgr0nedg  29456  wlkonl1iedg  29627  elwspths2on  29923  3cyclfrgrrn2  30249  isgrpo  30459  tpr2rico  33881  esumpcvgval  34047  omssubadd  34270  connpconn  35210  cvmliftlem15  35273  cvmlift2lem10  35287  satfdmlem  35343  fmla1  35362  satffunlem1lem2  35378  satffunlem2lem2  35381  fnessref  36333  fvineqsneq  37388  pibt2  37393  ptrecube  37602  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  fdc1  37728  sstotbnd3  37758  totbndss  37759  heibor1lem  37791  heibor1  37792  opidonOLD  37834  rngmgmbs4  37913  lvoli2  39563  paddss2  39800  lhpexle1lem  39989  lhpexle2lem  39991  dvhdimlem  41426  dvh3dim3N  41431  mapdh9a  41771  hdmap11lem2  41824  fiphp3d  42795  pell1qrss14  42844  minregex  43510  mnuop3d  44247  grumnudlem  44261  ismnushort  44277  eliuniin  45080  restuni3  45099  eliuniin2  45101  disjrnmpt2  45169  rnmptbd2lem  45229  ssfiunibd  45294  supminfxrrnmpt  45454  climrec  45588  islptre  45604  lptre2pt  45625  limsupmnfuzlem  45711  limsupre3lem  45717  limsupvaluz2  45723  supcnvlimsup  45725  liminfvalxr  45768  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  stoweidlem27  46012  stoweidlem29  46014  stoweidlem35  46020  stoweidlem48  46033  stoweidlem62  46047  fourierdlem48  46139  fourierdlem64  46155  fourierdlem65  46156  fourierdlem71  46162  fourierdlem73  46164  fourierdlem94  46185  fourierdlem103  46194  fourierdlem104  46195  fourierdlem112  46203  fourierdlem113  46204  sge0isum  46412  sge0seq  46431  meaiuninclem  46465  carageniuncllem2  46507  ovnsslelem  46545  hoidmvlelem1  46580  2reuimp  47103  afvelima  47155  sgoldbeven3prm  47771  nnsum4primes4  47777  nnsum4primesprm  47779  nnsum4primesgbe  47781  nnsum4primesle9  47783  grtriprop  47929  pgrpgt2nabl  48354  opnneilv  48897  sepnsepo  48912