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

Theorem ralimdva 2851
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)
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 ralimdva.1 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21ex 434 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32a2d 26 . 2  |-  ( ph  ->  ( ( x  e.  A  ->  ps )  ->  ( x  e.  A  ->  ch ) ) )
43ralimdv2 2850 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2798
This theorem is referenced by:  ralimdv  2853  ralimdvva  2854  wereu2  4866  fveqressseq  6012  f1mpt  6154  isores3  6216  caofrss  6558  caoftrn  6560  sorpssuni  6574  sorpssint  6575  onint  6615  smogt  7040  fisupg  7770  ixpfi2  7820  fissuni  7827  indexfi  7830  wemaplem2  7975  rankonidlem  8249  ac5num  8420  acni2  8430  acndom2  8438  alephle  8472  dfac5  8512  cfsmolem  8653  isf34lem7  8762  isf34lem6  8763  fin1a2s  8797  acncc  8823  ttukeylem6  8897  fpwwe2lem8  9018  gchina  9080  inar1  9156  tskord  9161  grudomon  9198  grur1a  9200  dedekind  9747  fimaxre  10497  uzwo  11155  uzwoOLD  11156  xrsupsslem  11509  xrinfmsslem  11510  fsuppmapnn0fiub0  12081  rexanre  13161  rexuz3  13163  rexico  13168  cau3lem  13169  limsupval2  13285  rlim2lt  13302  rlim3  13303  lo1bdd2  13329  lo1bddrp  13330  o1lo1  13342  climrlim2  13352  2clim  13377  o1co  13391  rlimcn1  13393  rlimcn2  13395  climcn1  13396  climcn2  13397  subcn2  13399  o1of2  13417  rlimo1  13421  o1rlimmul  13423  lo1add  13431  lo1mul  13432  climsqz  13445  climsqz2  13446  rlimsqzlem  13453  lo1le  13456  climbdd  13476  caucvgrlem  13477  caucvgrlem2  13479  caurcvg2  13482  iseralt  13489  cvgcmp  13612  cvgcmpce  13614  gcdcllem1  14131  pcfac  14400  pockthg  14406  infpnlem1  14410  prmreclem2  14417  prmreclem3  14418  vdwlem11  14491  vdwlem13  14493  vdwnnlem3  14497  isacs2  15032  acsfn1  15040  acsfn2  15042  catpropd  15086  drsdirfi  15546  ipodrsima  15774  isacs5  15781  mrelatglb  15793  mrelatlub  15795  isgrpinv  16079  issubg4  16199  gsmsymgreqlem2  16435  gexdvds  16583  gexcl3  16586  sylow2blem3  16621  cyggeninv  16865  gsummptnn0fz  16993  dprdff  17025  dprdffOLD  17031  issubdrg  17433  mptcoe1fsupp  18234  cply1coe0bi  18321  gsummoncoe1  18325  cygznlem3  18586  scmatdmat  18995  mdetdiagid  19080  mdetunilem9  19100  cpmatmcllem  19197  m2cpminvid2lem  19233  decpmatmulsumfsupp  19252  pmatcollpw1lem1  19253  pmatcollpw2lem  19256  pmatcollpwfi  19261  pm2mpf1  19278  mptcoe1matfsupp  19281  mp2pm2mplem4  19288  pm2mpmhmlem1  19297  pm2mp  19304  chpdmat  19320  chpscmat  19321  cpmidpmatlem3  19351  cayhamlem4  19367  neiptopnei  19611  cncnp  19759  isnrm2  19837  isreg2  19856  2ndcdisj  19935  islly2  19963  dislly  19976  kgen2ss  20034  ptbasfi  20060  ptclsg  20094  prdstopn  20107  txtube  20119  txlm  20127  isr0  20216  filuni  20364  alexsubALTlem3  20527  ptcmplem3  20532  ptcmplem4  20533  tsmsxplem1  20633  prdsmet  20851  metequiv2  20991  metcnpi3  21027  nmoleub  21216  rescncf  21379  cncfco  21389  evth  21437  lebnumlem3  21441  xlebnum  21443  nmoleub2lem2  21577  nmhmcn  21581  lmmcvg  21678  cmetcaulem  21705  caubl  21724  bcth3  21748  ovollb2lem  21877  ovoliunlem2  21892  ovolicc2lem3  21908  ovolicc2lem4  21909  nulmbl2  21925  volsup  21944  ioombl1lem4  21949  dyadmax  21985  vitalilem2  21996  vitalilem5  21999  mbfi1flimlem  22107  itg2seq  22127  itg2addlem  22143  itgcn  22227  limciun  22276  rolle  22369  dvfsumrlim  22410  itgsubst  22428  aannenlem1  22702  aalioulem3  22708  ulmcaulem  22767  ulmcau  22768  ulmss  22770  ulmbdd  22771  ulmcn  22772  ulmdvlem3  22775  mtest  22777  iblulm  22780  itgulm  22781  rlimcnp  23273  xrlimcnp  23276  rlimcxp  23281  o1cxp  23282  amgm  23298  ftalem2  23325  isppw2  23367  mumullem2  23432  2sqlem6  23622  chtppilimlem2  23637  chtppilim  23638  pntrsumbnd2  23730  pntlem3  23772  isperp2  24070  axeuclidlem  24243  axeuclid  24244  cusgrares  24450  edgwlk  24509  usgrnloop  24543  redwlk  24586  cusconngra  24654  wlkiswwlk1  24668  wlkiswwlk2lem4  24672  usg2wlkeq  24686  wwlknred  24701  wwlkm1edg  24713  clwlkisclwwlklem2a  24763  clwlkisclwwlklem1  24765  usgravd00  24897  cusgraisrusgra  24916  rusgraprop2  24920  rusgraprop3  24921  frisusgranb  24975  2pthfrgrarn  24987  2pthfrgrarn2  24988  2pthfrgra  24989  3cyclfrgra  24993  frgrancvvdeq  25020  frgrancvvdgeq  25021  nmoub3i  25666  ubthlem1  25764  ubthlem3  25766  ocsh  26179  chintcli  26227  chscllem2  26534  nmopub2tALT  26806  nmfnleub2  26823  lnconi  26930  riesz1  26962  rnbra  27004  leopadd  27029  leopmuli  27030  leoptr  27034  dmdbr3  27202  dmdbr4  27203  dmdbr5  27205  mdsl0  27207  mdsymlem6  27305  cdj1i  27330  xrge0infss  27558  cmppcmp  27839  lmxrge0  27912  lgambdd  28557  cvmlift2lem12  28737  finixpnum  30014  heicant  30025  itg2addnclem  30042  itg2addnclem3  30044  itg2addnc  30045  opnrebl2  30115  neibastop1  30153  neibastop2lem  30154  neibastop3  30156  filbcmb  30207  nninfnub  30220  geomcau  30228  sstotbnd2  30246  isbndx  30254  prdsbnd  30265  heibor1lem  30281  heiborlem1  30283  heibor  30293  rrncmslem  30304  intidl  30402  elrfirn2  30604  isnacs3  30618  rencldnfilem  30730  kelac1  30985  acsfn1p  31124  cvgdvgrat  31170  neglimc  31607  stoweidlem7  31743  fourierdlem73  31916  copisnmnd  32450  2zrngnmlid2  32584  ply1mulgsumlem1  32856  ply1mulgsumlem3  32858  ply1mulgsumlem4  32859  snlindsntor  32942  pclclN  35490  lauteq  35694  ltrnid  35734  mapdh9a  37392
  Copyright terms: Public domain W3C validator