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

Theorem rexlimdv3a 3026
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3023. (Contributed by NM, 7-Jun-2015.)
Hypothesis
Ref Expression
rexlimdv3a.1 ((𝜑𝑥𝐴𝜓) → 𝜒)
Assertion
Ref Expression
rexlimdv3a (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdv3a
StepHypRef Expression
1 rexlimdv3a.1 . . 3 ((𝜑𝑥𝐴𝜓) → 𝜒)
213exp 1261 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3023 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036  wcel 1987  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038  df-ex 1702  df-ral 2912  df-rex 2913
This theorem is referenced by:  sorpssuni  6902  sorpssint  6903  tcrank  8694  rpnnen1lem5  11765  rpnnen1lem5OLD  11771  hashfun  13167  resqrex  13928  resqrtcl  13931  prmgaplem6  15687  lbsextlem3  19082  cmpsublem  21115  cmpcld  21118  ovoliunlem2  23184  isblo3i  27517  trisegint  31798  itg2addnclem  33114  areacirclem2  33154  lshpnelb  33772  lsatfixedN  33797  lsmsatcv  33798  lssatomic  33799  lcv1  33829  lsatcvatlem  33837  islshpcv  33841  lfl1  33858  lshpsmreu  33897  lshpkrex  33906  lshpset2N  33907  lkrlspeqN  33959  cvrval3  34200  1cvratlt  34261  ps-2b  34269  llnnleat  34300  lvolex3N  34325  lplncvrlvol2  34402  osumcllem7N  34749  lhp0lt  34790  lhpj1  34809  4atexlemex6  34861  4atexlem7  34862  trlnidat  34961  cdlemd9  34994  cdleme21h  35123  cdlemg7fvbwN  35396  cdlemg7aN  35414  cdlemg34  35501  cdlemg36  35503  cdlemg44  35522  cdlemg48  35526  tendo1ne0  35617  cdlemk26-3  35695  cdlemk55b  35749  cdleml4N  35768  dih1dimatlem0  36118  dihglblem6  36130  dochshpncl  36174  dvh4dimlem  36233  dvh3dim2  36238  dvh3dim3N  36239  dochsatshpb  36242  dochexmidlem4  36253  dochexmidlem5  36254  dochexmidlem8  36257  dochkr1  36268  dochkr1OLDN  36269  lcfl7lem  36289  lcfl6  36290  lcfl8  36292  lcfrlem16  36348  lcfrlem40  36372  mapdval2N  36420  mapdrvallem2  36435  mapdpglem24  36494  mapdh6iN  36534  mapdh8ad  36569  mapdh8e  36574  hdmap1l6i  36609  hdmapval0  36626  hdmapevec  36628  hdmapval3N  36631  hdmap10lem  36632  hdmap11lem2  36635  hdmaprnlem15N  36654  hdmaprnlem16N  36655  hdmap14lem10  36670  hdmap14lem11  36671  hdmap14lem12  36672  hdmap14lem14  36674  hgmapval0  36685  hgmapval1  36686  hgmapadd  36687  hgmapmul  36688  hgmaprnlem3N  36691  hgmaprnlem4N  36692  hgmap11  36695  hgmapvvlem3  36718  rpnnen3lem  37099  dvconstbi  38036  expgrowth  38037  eliuniin  38783  limccog  39274  0ellimcdiv  39303  cosknegpi  39401  cncfshift  39408  cncfperiod  39413  cncfuni  39420  icccncfext  39421  dvbdfbdioolem1  39466  itgperiod  39520  stoweidlem57  39597  fourierdlem12  39659  fourierdlem48  39694  fourierdlem49  39695  fourierdlem52  39698  fourierdlem54  39700  fourierdlem68  39714  fourierdlem77  39723  fourierdlem83  39729  fourierdlem87  39733  fourierdlem102  39748  fourierdlem103  39749  fourierdlem104  39750  fourierdlem113  39759  fourierdlem114  39760  elaa2  39774  etransclem24  39798  etransclem32  39806  etransclem48  39822  sigarcol  40373
  Copyright terms: Public domain W3C validator