Theorem reximdv 3177

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3173	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  r19.12  3311  ss2rexv  3980  reusv3  5366  fvelima  6951  mpt3fvd  7689  iunpw  7786  frxp  8141  nnaordex2  8652  ssfiALT  9193  ordtypelem2  9517  wdom2d  9578  xpwdomg  9583  elhf4  9916  cff1  10340  iunfo  10627  nqereu  11018  reclem3pr  11138  map2psrpr  11199  supsrlem  11200  1re  11312  elss2prb  14637  exprelprel  14639  o1lo1  15710  rlimcn1  15761  subcn2  15768  lo1add  15800  lo1mul  15801  pythagtriplem19  17017  vdwnnlem2  17180  ramub2  17198  mgmidpfod  18863  sylow2alem2  19838  lsmless2x  19865  efgrelexlemb  19970  scmateALT  22833  decpmatmulsumfsupp  23097  pmatcollpw1lem1  23098  pmatcollpw2lem  23101  pm2mpmhmlem1  23142  cpmidpmatlem3  23196  cpmidgsum2  23203  tgcl  23293  neiss  23433  ssnei2  23440  tgcnp  23577  cnpco  23591  cnpresti  23612  lmcnp  23628  hausnei2  23677  1stcrest  23777  nlly2i  23801  llyss  23804  nllyss  23805  reftr  23839  lfinun  23850  txcnpi  23933  txcmplem1  23966  tx1stc  23975  nrmr0reg  24074  fbssfi  24162  fbfinnfr  24166  fgcl  24203  ufinffr  24254  elfm2  24273  fmfnfmlem1  24279  fmco  24286  fbflim2  24302  flffbas  24320  flftg  24321  cnpflf2  24325  alexsubALT  24376  cnextcn  24392  isucn2  24603  ucnima  24605  blssexps  24751  blssex  24752  mopni3  24819  neibl  24826  metss  24833  metcnp3  24865  cfilucfil  24884  metustbl  24891  psmetutop  24892  mpomulcn  25194  rescncf  25224  lebnum  25291  xlebnum  25292  lebnumii  25293  lmmbr  25585  fgcfil  25598  ovolsslem  25811  ovolunlem1  25824  ovoliunnul  25834  itgcn  26171  ellimc3  26205  c1lip3  26325  itgsubstlem  26374  plyss  26523  ulmclm  26720  ulmcau  26728  ulmcn  26732  rlimcxp  27307  chtppilimlem2  27807  chtppilim  27808  madess  28258  lrrecfr  28335  midex  29219  umgrnloop0  29693  usgrnloop0ALT  29792  uhgr2edg  29795  vtxduhgr0nedg  30079  wlkonl1iedg  30250  elwspths2on  30557  elwspths2onw  30558  3cyclfrgrrn2  30894  isgrpo  31105  tpr2rico  34591  esumpcvgval  34757  omssubadd  34979  r1filim  35782  fineqvnttrclse  35849  vonf1oonfo  35969  connpconn  36087  cvmliftlem15  36150  cvmlift2lem10  36164  satfdmlem  36220  fmla1  36239  satffunlem1lem2  36255  satffunlem2lem2  36258  fnessref  37238  ttctr  37374  fvineqsneq  38429  pibt2  38434  ptrecube  38632  poimirlem29  38661  poimirlem30  38662  poimirlem31  38663  dfprop2  38740  fdc1  38774  sstotbnd3  38804  totbndss  38805  heibor1lem  38837  heibor1  38838  opidonOLD  38880  rngmgmbs4  38959  lvoli2  40732  paddss2  40969  lhpexle1lem  41158  lhpexle2lem  41160  dvhdimlem  42595  dvh3dim3N  42600  mapdh9a  42940  hdmap11lem2  42993  fiphp3d  43920  pell1qrss14  43969  minregex  44629  mnuop3d  45349  grumnudlem  45363  ismnushort  45379  eliuniin  46208  restuni3  46227  eliuniin2  46229  disjrnmpt2  46297  rnmptbd2lem  46354  ssfiunibd  46419  supminfxrrnmpt  46575  climrec  46709  islptre  46725  lptre2pt  46744  limsupmnfuzlem  46830  limsupre3lem  46836  limsupvaluz2  46842  supcnvlimsup  46844  liminfvalxr  46887  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  stoweidlem27  47131  stoweidlem29  47133  stoweidlem35  47139  stoweidlem48  47152  stoweidlem62  47166  fourierdlem48  47258  fourierdlem64  47274  fourierdlem65  47275  fourierdlem71  47281  fourierdlem73  47283  fourierdlem94  47304  fourierdlem103  47313  fourierdlem104  47314  fourierdlem112  47322  fourierdlem113  47323  sge0isum  47531  sge0seq  47550  meaiuninclem  47584  carageniuncllem2  47626  ovnsslelem  47664  hoidmvlelem1  47699  2reuimp  48279  afvelima  48331  sgoldbeven3prm  48975  nnsum4primes4  48981  nnsum4primesprm  48983  nnsum4primesgbe  48985  nnsum4primesle9  48987  grtriprop  49133  pgrpgt2nabl  49572  opnneilv  50117  sepnsepo  50132