Theorem reximdv 3201

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  r19.12  3252  r19.12OLD  3253  ss2rexv  3986  reusv3  5323  fvelima  6817  iunpw  7599  frxp  7938  ssfiALT  8919  ordtypelem2  9208  wdom2d  9269  xpwdomg  9274  cff1  9945  iunfo  10226  nqereu  10616  reclem3pr  10736  map2psrpr  10797  supsrlem  10798  1re  10906  elss2prb  14129  exprelprel  14131  o1lo1  15174  rlimcn1  15225  subcn2  15232  lo1add  15264  lo1mul  15265  pythagtriplem19  16462  vdwnnlem2  16625  ramub2  16643  sylow2alem2  19138  lsmless2x  19165  efgrelexlemb  19271  scmateALT  21569  decpmatmulsumfsupp  21830  pmatcollpw1lem1  21831  pmatcollpw2lem  21834  pm2mpmhmlem1  21875  cpmidpmatlem3  21929  cpmidgsum2  21936  tgcl  22027  neiss  22168  ssnei2  22175  tgcnp  22312  cnpco  22326  cnpresti  22347  lmcnp  22363  hausnei2  22412  1stcrest  22512  nlly2i  22535  llyss  22538  nllyss  22539  reftr  22573  lfinun  22584  txcnpi  22667  txcmplem1  22700  tx1stc  22709  nrmr0reg  22808  fbssfi  22896  fbfinnfr  22900  fgcl  22937  ufinffr  22988  elfm2  23007  fmfnfmlem1  23013  fmco  23020  fbflim2  23036  flffbas  23054  flftg  23055  cnpflf2  23059  alexsubALT  23110  cnextcn  23126  isucn2  23339  ucnima  23341  blssexps  23487  blssex  23488  mopni3  23556  neibl  23563  metss  23570  metcnp3  23602  cfilucfil  23621  metustbl  23628  psmetutop  23629  rescncf  23966  lebnum  24033  xlebnum  24034  lebnumii  24035  lmmbr  24327  fgcfil  24340  ovolsslem  24553  ovolunlem1  24566  ovoliunnul  24576  itgcn  24914  ellimc3  24948  c1lip3  25068  itgsubstlem  25117  plyss  25265  ulmclm  25451  ulmcau  25459  ulmcn  25463  rlimcxp  26028  chtppilimlem2  26527  chtppilim  26528  midex  27002  umgrnloop0  27382  usgrnloop0ALT  27475  uhgr2edg  27478  vtxduhgr0nedg  27762  wlkonl1iedg  27935  elwspths2on  28226  3cyclfrgrrn2  28552  isgrpo  28760  tpr2rico  31764  esumpcvgval  31946  omssubadd  32167  connpconn  33097  cvmliftlem15  33160  cvmlift2lem10  33174  satfdmlem  33230  fmla1  33249  satffunlem1lem2  33265  satffunlem2lem2  33268  madess  33986  lrrecfr  34027  fnessref  34473  fvineqsneq  35510  pibt2  35515  ptrecube  35704  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  fdc1  35831  sstotbnd3  35861  totbndss  35862  heibor1lem  35894  heibor1  35895  opidonOLD  35937  rngmgmbs4  36016  lvoli2  37522  paddss2  37759  lhpexle1lem  37948  lhpexle2lem  37950  dvhdimlem  39385  dvh3dim3N  39390  mapdh9a  39730  hdmap11lem2  39783  sn-negex12  40319  fiphp3d  40557  pell1qrss14  40606  mnuop3d  41778  grumnudlem  41792  ismnushort  41808  eliuniin  42538  restuni3  42556  eliuniin2  42558  disjrnmpt2  42615  rnmptbd2lem  42683  ssfiunibd  42738  supminfxrrnmpt  42901  climrec  43034  islptre  43050  lptre2pt  43071  limsupmnfuzlem  43157  limsupre3lem  43163  limsupvaluz2  43169  supcnvlimsup  43171  liminfvalxr  43214  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem27  43458  stoweidlem29  43460  stoweidlem35  43466  stoweidlem48  43479  stoweidlem62  43493  fourierdlem48  43585  fourierdlem64  43601  fourierdlem65  43602  fourierdlem71  43608  fourierdlem73  43610  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  sge0isum  43855  sge0seq  43874  meaiuninclem  43908  carageniuncllem2  43950  ovnsslelem  43988  hoidmvlelem1  44023  2reuimp  44494  afvelima  44546  sgoldbeven3prm  45123  nnsum4primes4  45129  nnsum4primesprm  45131  nnsum4primesgbe  45133  nnsum4primesle9  45135  pgrpgt2nabl  45590  opnneilv  46090  sepnsepo  46105