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

Theorem reximdv 2998
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 2997 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  r19.12  3044  reusv3  4797  fvelima  6143  iunpw  6847  frxp  7151  ssfi  8042  ordtypelem2  8284  wdom2d  8345  xpwdomg  8350  cff1  8940  iunfo  9217  nqereu  9607  reclem3pr  9727  map2psrpr  9787  supsrlem  9788  1re  9895  elss2prb  13073  exprelprel  13076  o1lo1  14062  rlimcn1  14113  subcn2  14119  lo1add  14151  lo1mul  14152  pythagtriplem19  15322  vdwnnlem2  15484  ramub2  15502  sylow2alem2  17802  lsmless2x  17829  efgrelexlemb  17932  scmateALT  20079  decpmatmulsumfsupp  20339  pmatcollpw1lem1  20340  pmatcollpw2lem  20343  pm2mpmhmlem1  20384  cpmidpmatlem3  20438  cpmidgsum2  20445  tgcl  20526  neiss  20665  ssnei2  20672  tgcnp  20809  cnpco  20823  cnpresti  20844  lmcnp  20860  hausnei2  20909  1stcrest  21008  nlly2i  21031  llyss  21034  nllyss  21035  reftr  21069  lfinun  21080  txcnpi  21163  txcmplem1  21196  tx1stc  21205  nrmr0reg  21304  fbssfi  21393  fbfinnfr  21397  fgcl  21434  ufinffr  21485  elfm2  21504  fmfnfmlem1  21510  fmco  21517  fbflim2  21533  flffbas  21551  flftg  21552  cnpflf2  21556  alexsubALT  21607  cnextcn  21623  isucn2  21835  ucnima  21837  blssexps  21982  blssex  21983  mopni3  22050  neibl  22057  metss  22064  metcnp3  22096  cfilucfil  22115  metustbl  22122  psmetutop  22123  rescncf  22439  lebnum  22502  xlebnum  22503  lebnumii  22504  lmmbr  22782  fgcfil  22795  ovolsslem  22976  ovolunlem1  22989  ovoliunnul  22999  itgcn  23332  ellimc3  23366  c1lip3  23483  itgsubstlem  23532  plyss  23676  ulmclm  23862  ulmcau  23870  ulmcn  23874  rlimcxp  24417  chtppilimlem2  24880  chtppilim  24881  midex  25347  usgranloop0  25675  usgra2edg  25677  3v3e3cycl1  25938  4cycl4v4e  25960  4cycl4dv4e  25962  vdusgra0nedg  26201  usgravd0nedg  26211  3cyclfrgrarn2  26307  vdn0frgrav2  26316  vdgn0frgrav2  26317  frgrawopreg1  26343  frgrawopreg2  26344  isgrpo  26501  tpr2rico  29092  esumpcvgval  29273  omssubadd  29495  conpcon  30277  cvmliftlem15  30340  cvmlift2lem10  30354  fnessref  31328  ptrecube  32382  poimirlem29  32411  poimirlem30  32412  poimirlem31  32413  fdc1  32515  sstotbnd3  32548  totbndss  32549  heibor1lem  32581  heibor1  32582  opidonOLD  32624  rngmgmbs4  32703  lvoli2  33688  paddss2  33925  lhpexle1lem  34114  lhpexle2lem  34116  dvhdimlem  35554  dvh3dim3N  35559  mapdh9a  35900  hdmap11lem2  35955  fiphp3d  36204  pell1qrss14  36253  eliuniin  38110  restuni3  38136  eliuniin2  38138  disjrnmpt2  38173  ssfiunibd  38267  climrec  38474  islptre  38490  lptre2pt  38511  ioodvbdlimc1lem2  38626  ioodvbdlimc2lem  38628  stoweidlem27  38724  stoweidlem29  38726  stoweidlem35  38732  stoweidlem48  38745  stoweidlem62  38759  fourierdlem48  38851  fourierdlem64  38867  fourierdlem65  38868  fourierdlem71  38874  fourierdlem73  38876  fourierdlem94  38897  fourierdlem103  38906  fourierdlem104  38907  fourierdlem112  38915  fourierdlem113  38916  sge0isum  39124  sge0seq  39143  meaiuninclem  39177  carageniuncllem2  39216  ovnsslelem  39254  hoidmvlelem1  39289  afvelima  39701  nnsum4primes4  40010  nnsum4primesprm  40012  nnsum4primesgbe  40014  nnsum4primesle9  40016  umgrnloop0  40336  usgrnloop0ALT  40434  uhgr2edg  40437  vtxduhgr0nedg  40709  wlkOnl1iedg  40875  elwspths2on  41165  3cyclfrgrrn2  41459  frgrwopreg1  41489  frgrwopreg2  41490  pgrpgt2nabl  41943
  Copyright terms: Public domain W3C validator