MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimd Structured version   Unicode version

Theorem rexlimd 2909
Description: Deduction form of rexlimd 2909. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)
Hypotheses
Ref Expression
rexlimd.1  |-  F/ x ph
rexlimd.2  |-  F/ x ch
rexlimd.3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
rexlimd  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )

Proof of Theorem rexlimd
StepHypRef Expression
1 rexlimd.1 . 2  |-  F/ x ph
2 rexlimd.2 . . 3  |-  F/ x ch
32a1i 11 . 2  |-  ( ph  ->  F/ x ch )
4 rexlimd.3 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
51, 3, 4rexlimd2 2908 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1663    e. wcel 1868   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-12 1905
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-ral 2780  df-rex 2781
This theorem is referenced by:  rexlimdvOLD  2916  r19.29af2  2966  reusv2lem2  4622  ralxfrALT  4636  fvmptt  5977  ffnfv  6060  peano5  6726  tz7.49  7166  nneneq  7757  ac6sfi  7817  ixpiunwdom  8108  r1val1  8258  rankuni2b  8325  infpssrlem4  8736  zorn2lem4  8929  zorn2lem5  8930  konigthlem  8993  tskuni  9208  gruiin  9235  lbzbi  11252  fprodle  14037  iunconlem  20428  ptbasfi  20582  alexsubALTlem3  21050  ovoliunnul  22446  iunmbl2  22496  mptelee  24911  atom1d  27991  elabreximd  28130  iundisjf  28188  esumc  28867  poimirlem24  31877  poimirlem26  31879  poimirlem27  31880  heicant  31888  indexa  31973  sdclem2  31984  glbconxN  32861  cdleme26ee  33845  cdleme32d  33929  cdleme32f  33931  cdlemk38  34400  cdlemk19x  34428  cdlemk11t  34431  refsumcn  37211  suprnmpt  37287  dffo3f  37299  wessf1ornlem  37308  disjf1o  37315  disjinfi  37317  upbdrech  37364  ssfiunibd  37368  iuneqfzuzlem  37398  infrpge  37415  iccshift  37449  iooshift  37453  fmul01lt1  37483  islptre  37518  rexlim2d  37524  limcperiod  37527  islpcn  37538  limclner  37551  dvnprodlem1  37640  dvnprodlem2  37641  itgperiod  37677  stoweidlem29  37708  stoweidlem29OLD  37709  stoweidlem31  37711  stoweidlem59  37739  stirlinglem13  37767  fourierdlem48  37837  fourierdlem51  37840  fourierdlem53  37842  fourierdlem80  37869  fourierdlem81  37870  fourierdlem93  37882  elaa2  37918  sge00  38005  sge0f1o  38011  sge0gerp  38024  sge0lefi  38027  sge0ltfirp  38029  sge0resplit  38035  sge0iunmptlemre  38044  sge0iunmpt  38047  sge0isum  38056  sge0xp  38058  iundjiun  38076  isomenndlem  38129  ovncvrrp  38160  ovnsubaddlem1  38166  ffnafv  38384  iccpartdisj  38462  2zrngagrp  39214
  Copyright terms: Public domain W3C validator