MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximdv Structured version   Visualization version   GIF version

Theorem reximdv 3045
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
StepHypRef Expression
1 reximdv.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 25 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32reximdvai 3044 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  r19.12  3092  reusv3  4906  fvelima  6287  iunpw  7020  frxp  7332  ssfi  8221  ordtypelem2  8465  wdom2d  8526  xpwdomg  8531  cff1  9118  iunfo  9399  nqereu  9789  reclem3pr  9909  map2psrpr  9969  supsrlem  9970  1re  10077  elss2prb  13307  exprelprel  13309  o1lo1  14312  rlimcn1  14363  subcn2  14369  lo1add  14401  lo1mul  14402  pythagtriplem19  15585  vdwnnlem2  15747  ramub2  15765  sylow2alem2  18079  lsmless2x  18106  efgrelexlemb  18209  scmateALT  20366  decpmatmulsumfsupp  20626  pmatcollpw1lem1  20627  pmatcollpw2lem  20630  pm2mpmhmlem1  20671  cpmidpmatlem3  20725  cpmidgsum2  20732  tgcl  20821  neiss  20961  ssnei2  20968  tgcnp  21105  cnpco  21119  cnpresti  21140  lmcnp  21156  hausnei2  21205  1stcrest  21304  nlly2i  21327  llyss  21330  nllyss  21331  reftr  21365  lfinun  21376  txcnpi  21459  txcmplem1  21492  tx1stc  21501  nrmr0reg  21600  fbssfi  21688  fbfinnfr  21692  fgcl  21729  ufinffr  21780  elfm2  21799  fmfnfmlem1  21805  fmco  21812  fbflim2  21828  flffbas  21846  flftg  21847  cnpflf2  21851  alexsubALT  21902  cnextcn  21918  isucn2  22130  ucnima  22132  blssexps  22278  blssex  22279  mopni3  22346  neibl  22353  metss  22360  metcnp3  22392  cfilucfil  22411  metustbl  22418  psmetutop  22419  rescncf  22747  lebnum  22810  xlebnum  22811  lebnumii  22812  lmmbr  23102  fgcfil  23115  ovolsslem  23298  ovolunlem1  23311  ovoliunnul  23321  itgcn  23654  ellimc3  23688  c1lip3  23807  itgsubstlem  23856  plyss  24000  ulmclm  24186  ulmcau  24194  ulmcn  24198  rlimcxp  24745  chtppilimlem2  25208  chtppilim  25209  midex  25674  umgrnloop0  26049  usgrnloop0ALT  26142  uhgr2edg  26145  vtxduhgr0nedg  26444  wlkonl1iedg  26617  elwspths2on  26926  3cyclfrgrrn2  27267  isgrpo  27479  tpr2rico  30086  esumpcvgval  30268  omssubadd  30490  connpconn  31343  cvmliftlem15  31406  cvmlift2lem10  31420  fnessref  32477  ptrecube  33539  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  fdc1  33672  sstotbnd3  33705  totbndss  33706  heibor1lem  33738  heibor1  33739  opidonOLD  33781  rngmgmbs4  33860  lvoli2  35185  paddss2  35422  lhpexle1lem  35611  lhpexle2lem  35613  dvhdimlem  37050  dvh3dim3N  37055  mapdh9a  37396  hdmap11lem2  37451  fiphp3d  37700  pell1qrss14  37749  eliuniin  39593  restuni3  39615  eliuniin2  39617  disjrnmpt2  39689  rnmptbd2lem  39777  ssfiunibd  39837  supminfxrrnmpt  40014  climrec  40153  islptre  40169  lptre2pt  40190  limsupmnfuzlem  40276  limsupre3lem  40282  limsupvaluz2  40288  supcnvlimsup  40290  liminfvalxr  40333  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem27  40562  stoweidlem29  40564  stoweidlem35  40570  stoweidlem48  40583  stoweidlem62  40597  fourierdlem48  40689  fourierdlem64  40705  fourierdlem65  40706  fourierdlem71  40712  fourierdlem73  40714  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem113  40754  sge0isum  40962  sge0seq  40981  meaiuninclem  41015  carageniuncllem2  41057  ovnsslelem  41095  hoidmvlelem1  41130  afvelima  41568  sgoldbeven3prm  41996  nnsum4primes4  42002  nnsum4primesprm  42004  nnsum4primesgbe  42006  nnsum4primesle9  42008  pgrpgt2nabl  42472
  Copyright terms: Public domain W3C validator