Theorem reximdva 3178

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
ralimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
reximdva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		ralimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 417	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3176	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  reximddv  3181  reximdvva  3213  reximddv2  3224  wereu2  5648  frpomin  6330  dffo4  7088  nnaordex  8612  frfi  9233  fisupg  9236  marypha1  9382  fiinfg  9449  wemapsolem  9500  unwdomg  9534  rankr1ai  9758  cofsmo  10241  cfcoflem  10244  inar1  10748  nqerf  10903  prlem936  11020  fimaxre  12147  fiminre  12150  arch  12489  bndndx  12491  suprfinzcl  12698  zmin  12956  elpq  12987  qbtwnxr  13214  qsqueeze  13215  qextltlem  13216  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  supxrunb1  13333  ssnn0fi  14009  fsuppmapnn0fiub0  14017  fsuppmapnn0fz  14020  expnlbnd2  14258  r19.29uz  15390  cau3lem  15394  rlim2lt  15536  rlimclim  15585  2clim  15611  o1co  15625  climcn1  15631  climcn2  15632  rlimo1  15656  climsqz  15680  climsqz2  15681  rlimsqzlem  15688  lo1le  15691  climsup  15709  climcau  15710  caucvgrlem2  15714  iseralt  15724  cvgcmp  15856  cvgcmpce  15858  supcvg  15898  rpnnen2lem12  16269  bezoutlem1  16585  divgcdcoprmex  16712  exprmfct  16751  prmdvdsfz  16752  prmdvdsncoprmbd  16774  pclem  16886  pc2dvds  16927  pcprmpw  16931  dvdsprmpweqle  16934  unbenlem  16956  infpnlem2  16959  infpn2  16961  prmunb  16962  vdwlem2  17030  ramub1lem2  17075  prmdvdsprmop  17091  prmgaplem7  17105  ipodrsima  18585  smndex1mgm  18957  grpinveu  19029  dfgrp3lem  19092  psgneu  19564  odbezout  19616  sylow2blem3  19680  nn0gsumfz  20042  irredrmul  20497  zrninitoringc  20749  lbsextlem2  21249  znunit  21670  mptcoe1fsupp  22332  evls1fpws  22486  scmate  22624  scmatscm  22627  scmatfo  22644  mat1scmat  22653  pmatcoe1fsupp  22815  pmatcollpwfi  22896  pmatcollpw3fi  22899  mptcoe1matfsupp  22916  pm2mp  22939  chmaidscmat  22962  cpmadumatpoly  22997  chcoeffeq  23000  cayhamlem3  23001  cayhamlem4  23002  neiptopnei  23246  neitr  23294  cnpnei  23378  haust1  23466  isnrm3  23473  isreg2  23491  tgcmp  23515  hauscmplem  23520  hauscmp  23521  bwth  23524  1stcfb  23559  1stcelcls  23575  lly1stc  23610  txcmplem1  23755  txlm  23762  xkococnlem  23773  filuni  23999  filufint  24034  ufilen  24044  fclscf  24139  cnextcn  24181  ustex2sym  24331  ustex3sym  24332  utopreg  24366  isucn2  24392  ucnima  24394  ucncn  24398  neipcfilu  24409  metequiv2  24624  metrest  24638  xrsmopn  24927  mulc1cncf  25021  cncfco  25023  bndth  25074  lmmcvg  25377  cfil3i  25385  iscau4  25395  cmetcaulem  25404  iscmet3lem1  25407  caussi  25413  equivcfil  25415  equivcau  25416  caubl  25424  minveclem3b  25544  ovolgelb  25596  ovollb2lem  25604  ovolctb  25606  ovolicc2lem4  25636  ioombl1lem4  25677  dyadmax  25714  volsup2  25721  itg2monolem1  25866  c1liplem1  26112  c1lip1  26113  dvivthlem1  26124  lhop1  26130  ftc1a  26153  ftc1lem6  26157  ply1divex  26251  elply2  26310  dgrlem  26343  aacjcl  26445  aalioulem2  26451  aalioulem3  26452  aalioulem4  26453  ulmcaulem  26511  ulmcau  26512  ulmss  26514  mtest  26521  itgulm  26525  reeff1o  26564  efif1olem4  26664  rlimcnp  27084  xrlimcnp  27087  lgamucov  27156  ftalem3  27193  fta  27198  muval1  27251  dvdssqf  27256  mumullem1  27297  lgsqrmod  27470  lgsqrmodndvds  27471  pntlem3  27727  ostth  27757  nosupno  27821  nosupbnd1lem4  27829  noinfno  27836  noinfbnd1lem4  27844  conway  27926  etaslts  27940  znegscl  28539  tgtrisegint  28722  tgbtwndiff  28729  tgcgrxfr  28741  lnext  28790  legov2  28809  legtrd  28812  hlcgrex  28839  colperpexlem3  28959  colperpex  28960  hlpasch  28983  hpgerlem  28992  hpgtr  28995  dfcgra2  29078  acopy  29081  inagswap  29089  inaghl  29093  cgrg3col4  29101  axpasch  29196  wwlksnredwwlkn0  30150  midwwlks2s3  30206  clwwlkn1loopb  30299  2pthfrgrrn2  30539  frgrwopreg1  30574  frgrwopreg2  30575  grpoidinvlem3  30763  grpoideu  30766  grpoinveu  30776  ubthlem1  31127  minvecolem5  31138  htthlem  31174  chscllem2  31895  nmopun  32271  lnconi  32290  rnbra  32364  sumdmdii  32672  cdj3lem2b  32694  foresf1o  32756  acunirnmpt  32912  xrofsup  33020  fprodex01  33077  mndlactfo  33255  mndractfo  33257  isarchi3  33415  isarchiofld  33427  erler  33493  erld2  33494  dfufd2lem  33751  constrconj  34047  constrextdg2lem  34050  constrcjcl  34070  lmxrge0  34254  lmdvg  34255  esumlub  34362  esumfsup  34372  esumcvg  34388  ftc2re  34897  cusgr3cyclex  35494  cvmliftmolem2  35640  cvmlift2lem12  35672  satfv1  35721  satffunlem1lem2  35761  satffunlem2lem2  35764  satfv0fvfmla0  35771  ellcsrspsn  35999  r1peuqusdeg1  36001  wzel  36180  wsuclem  36181  btwndiff  36385  trisegint  36386  cgrxfr  36413  lineext  36434  segcon2  36463  brsegle2  36467  seglecgr12im  36468  segletr  36472  broutsideof3  36484  opnrebl2  36689  nn0prpw  36691  fin2so  38113  poimirlem27  38153  poimirlem30  38156  poimirlem31  38157  poimir  38159  mblfinlem1  38163  mblfinlem2  38164  mblfinlem3  38165  mblfinlem4  38166  itg2addnclem  38177  ftc1cnnc  38198  ftc1anclem5  38203  sdclem1  38249  geomcau  38265  equivtotbnd  38284  bndss  38292  ismtybndlem  38312  heibor1lem  38315  rrncmslem  38338  rngo2  38413  prtlem15  39506  lsateln0  39626  lsat0cv  39664  eqlkr3  39732  lkrshp  39736  lshpset2N  39750  hlhgt2  40020  hlrelat2  40034  atle  40067  athgt  40087  2dim  40101  1cvratex  40104  ps-2  40109  dalem20  40324  lhpexle1lem  40638  lhpexle1  40639  lhpexle2lem  40640  lhpmcvr5N  40658  lhpmcvr6N  40659  cdleme25a  40984  cdleme29ex  41005  cdlemfnid  41195  cdlemg33b0  41332  cdlemg33a  41337  cdlemg35  41344  cdleml3N  41609  dihlsscpre  41865  dih1dimb2  41872  dihatexv  41969  dvh3dim2  42079  dochkr1  42109  dochkr1OLDN  42110  lcfl8  42133  lcfl8b  42135  lcfrlem5  42177  lcfrlem6  42178  mapdrvallem2  42276  mapdh9a  42420  mapdh9aOLDN  42421  hdmaprnlem3eN  42489  hdmaprnlem16N  42493  mndmolinv  42719  primrootsunit1  42721  flt4lem5elem  43240  flt4lem7  43248  nna4b4nsq  43249  fphpdo  43401  rencldnfilem  43404  irrapxlem2  43407  oasubex  43870  tfsconcatlem  43920  tfsconcatrev  43932  cvgdvgrat  44882  expgrowth  44904  projf1o  45773  ssfiunibd  45887  supxrgere  45908  supxrgelem  45912  suplesup  45914  infrpge  45926  infleinf  45946  supxrunb3  45973  unb2ltle  45988  uzub  46004  cvgcaule  46064  qinioo  46110  qelioo  46121  climinf  46181  mullimc  46191  islptre  46194  limccog  46195  mullimcf  46198  limcrecl  46204  sumnnodd  46205  neglimc  46220  0ellimcdiv  46222  limclner  46224  allbutfifvre  46248  climleltrp  46249  fnlimabslt  46252  climinf2lem  46279  limsuppnflem  46283  limsupvaluz2  46311  supcnvlimsup  46313  limsupgtlem  46350  liminflelimsupuz  46358  liminflimsupclim  46380  limsupub2  46385  xlimpnfxnegmnf  46387  cncfioobd  46470  stoweidlem7  46580  stoweidlem27  46600  stoweidlem39  46612  stoweidlem48  46621  stoweidlem49  46622  stoweidlem60  46633  stoweidlem61  46634  stoweid  46636  dirkercncflem2  46677  fourierdlem20  46700  fourierdlem39  46719  fourierdlem41  46721  fourierdlem48  46727  fourierdlem49  46728  fourierdlem50  46729  fourierdlem64  46743  fourierdlem73  46752  fourierdlem74  46753  fourierdlem75  46754  fourierdlem87  46766  fourierdlem103  46782  fourierdlem104  46783  qndenserrnopnlem  46870  sge0ltfirp  46973  sge0gerpmpt  46975  sge0ltfirpmpt2  46999  sge0isum  47000  sge0pnffigtmpt  47013  sge0pnffsumgt  47015  sge0gtfsumgt  47016  sge0uzfsumgt  47017  nnfoctbdjlem  47028  meaiuninclem  47053  meaiuninc3v  47057  omeiunltfirp  47092  carageniuncllem2  47095  volicorescl  47126  hoidmv1le  47167  hoidmvlelem3  47170  hoiqssbllem3  47197  hspmbllem2  47200  iunhoiioolem  47248  vonioo  47255  vonicc  47258  smfaddlem1  47336  smflimlem2  47345  smflimlem3  47346  smfmullem4  47367  fsetsnfo  47646  2reu8i  47706  imasetpreimafvbijlemfo  48010  2pwp1prmfmtno  48198  proththd  48222  sbgoldbwt  48398  sbgoldbst  48399  sbgoldbalt  48402  bgoldbtbndlem4  48429  bgoldbtbnd  48430  grtriprop  48562  ply1mulgsumlem3  49020  ply1mulgsumlem4  49021  islindeps2  49115  isldepslvec2  49117