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

Theorem ralimdva 2592
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
ralimdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ralimdva  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ralimdva
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 ralimdva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
31, 2ralimdaa 2591 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   A.wral 2516
This theorem is referenced by:  ralimdv  2593  wereu2  4327  onint  4523  f1mpt  5684  isores3  5731  caofrss  6009  caoftrn  6011  sorpssuni  6185  sorpssint  6186  smogt  6317  tfrlem1  6324  fisupg  7038  ixpfi2  7087  fissuni  7093  indexfi  7096  wemaplem2  7195  rankonidlem  7433  ac5num  7596  acni2  7606  acndom2  7614  alephle  7648  dfac5  7688  cfsmolem  7829  isf34lem7  7938  isf34lem6  7939  fin1a2s  7973  acncc  7999  ttukeylem6  8074  fpwwe2lem8  8192  gchina  8254  inar1  8330  tskord  8335  grudomon  8372  grur1a  8374  fimaxre  9634  uzwo  10213  uzwoOLD  10214  xrsupsslem  10556  xrinfmsslem  10557  rexanre  11760  rexuz3  11762  rexico  11767  cau3lem  11768  limsupval2  11884  rlim2lt  11901  rlim3  11902  lo1bdd2  11928  lo1bddrp  11929  o1lo1  11941  climrlim2  11951  2clim  11976  o1co  11990  rlimcn1  11992  rlimcn2  11994  climcn1  11995  climcn2  11996  subcn2  11998  o1of2  12016  rlimo1  12020  o1rlimmul  12022  lo1add  12030  lo1mul  12031  climsqz  12044  climsqz2  12045  rlimsqzlem  12052  lo1le  12055  caucvgrlem  12075  caucvgrlem2  12077  caurcvg2  12080  iseralt  12087  cvgcmp  12204  cvgcmpce  12206  gcdcllem1  12617  pcfac  12874  pockthg  12880  infpnlem1  12884  prmreclem2  12891  prmreclem3  12892  vdwlem11  12965  vdwlem13  12967  vdwnnlem3  12971  isacs2  13482  acsfn1  13490  acsfn2  13492  catpropd  13539  drsdirfi  13999  ipodrsima  14195  isacs5  14202  mrelatglb  14214  mrelatlub  14216  isgrpinv  14459  issubg4  14565  gexdvds  14822  gexcl3  14825  sylow2blem3  14860  cyggeninv  15097  dprdff  15174  issubdrg  15497  islmhm2  15722  cygznlem3  16450  cncnp  16936  isnrm2  17013  isreg2  17032  2ndcdisj  17109  islly2  17137  dislly  17150  kgen2ss  17177  ptbasfi  17203  ptclsg  17236  prdstopn  17249  txtube  17261  txlm  17269  isr0  17355  filuni  17507  alexsubALTlem3  17670  ptcmplem3  17675  ptcmplem4  17676  tgpt0  17728  tsmsxplem1  17762  prdsmet  17861  metequiv2  17983  metcnpi3  18019  isngp4  18060  nmoleub  18167  addcnlem  18295  rescncf  18328  cncfco  18338  evth  18384  lebnumlem3  18388  xlebnum  18390  nmoleub2lem2  18524  nmhmcn  18528  lmmcvg  18614  cmetcaulem  18641  caubl  18660  bcth3  18680  ovollb2lem  18774  ovoliunlem2  18789  ovolicc2lem3  18805  ovolicc2lem4  18806  nulmbl2  18821  volsup  18840  ioombl1lem4  18845  dyadmax  18880  vitalilem2  18891  vitalilem5  18894  mbfi1flimlem  19004  itg2seq  19024  itg2addlem  19040  itgcn  19124  limciun  19171  rolle  19264  c1lip3  19273  dvfsumrlim  19305  itgsubst  19323  aannenlem1  19635  aalioulem2  19640  aalioulem3  19641  aalioulem5  19643  aalioulem6  19644  aaliou  19645  ulmcaulem  19698  ulmcau  19699  ulmss  19701  ulmbdd  19702  ulmcn  19703  ulmdvlem3  19706  mtest  19708  iblulm  19710  itgulm  19711  rlimcnp  20187  xrlimcnp  20190  rlimcxp  20195  o1cxp  20196  amgm  20212  ftalem2  20238  isppw2  20280  mumullem2  20345  2sqlem6  20535  chtppilimlem2  20550  chtppilim  20551  pntrsumbnd2  20643  pntlem3  20685  nmoub3i  21276  ubthlem1  21374  ubthlem3  21376  ocsh  21787  chintcli  21835  chscllem2  22160  nmopub2tALT  22414  nmfnleub2  22431  lnconi  22538  riesz1  22570  rnbra  22612  leopadd  22637  leopmuli  22638  leoptr  22642  dmdbr3  22810  dmdbr4  22811  dmdbr5  22813  mdsl0  22815  mdsymlem6  22913  cdj1i  22938  cvmlift2lem12  23182  dedekind  23418  dedekindle  23419  axfelem8  23687  axeuclidlem  23930  axeuclid  23931  mgmlion  24669  intfmu2  24851  islimrs3  24913  islimrs4  24914  icmpmon  25148  bhp3  25509  opnrebl2  25568  neibastop1  25640  neibastop2lem  25641  neibastop3  25643  filbcmb  25764  nninfnub  25793  geomcau  25807  sstotbnd2  25830  isbndx  25838  equivbnd  25846  prdsbnd  25849  heibor1lem  25865  heiborlem1  25867  heibor  25877  rrncmslem  25888  ghomco  25905  intidl  25986  elrfirn2  26103  isnacs3  26117  rencldnfilem  26235  kelac1  26493  acsfn1p  26839  stoweidlem7  27056  pclclN  29210  lauteq  29414  ltrnid  29454  mapdh9a  31110
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-ral 2520
  Copyright terms: Public domain W3C validator