Theorem reximdva 3181

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 418	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3179	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093

This theorem is used by:  reximddv  3184  reximdvva  3216  reximddv2  3227  wereu2  5663  frpomin  6348  dffo4  7105  nnaordex  8633  frfi  9255  fisupg  9258  marypha1  9404  fiinfg  9471  wemapsolem  9522  unwdomg  9556  rankr1ai  9780  cofsmo  10271  cfcoflem  10274  inar1  10778  nqerf  10933  prlem936  11050  fimaxre  12177  fiminre  12180  arch  12519  bndndx  12521  suprfinzcl  12728  zmin  12986  elpq  13017  qbtwnxr  13244  qsqueeze  13245  qextltlem  13246  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  supxrunb1  13363  ssnn0fi  14041  fsuppmapnn0fiub0  14049  fsuppmapnn0fz  14052  expnlbnd2  14290  r19.29uz  15428  cau3lem  15432  rlim2lt  15574  rlimclim  15623  2clim  15649  o1co  15663  climcn1  15669  climcn2  15670  rlimo1  15694  climsqz  15718  climsqz2  15719  rlimsqzlem  15726  lo1le  15729  climsup  15747  climcau  15748  caucvgrlem2  15752  iseralt  15762  cvgcmp  15894  cvgcmpce  15896  supcvg  15936  rpnnen2lem12  16306  bezoutlem1  16622  divgcdcoprmex  16749  exprmfct  16788  prmdvdsfz  16789  prmdvdsncoprmbd  16811  pclem  16923  pc2dvds  16964  pcprmpw  16968  dvdsprmpweqle  16971  unbenlem  16993  infpnlem2  16996  infpn2  16998  prmunb  16999  vdwlem2  17067  ramub1lem2  17112  prmdvdsprmop  17128  prmgaplem7  17142  ipodrsima  18622  smndex1mgm  19000  grpinveu  19072  dfgrp3lem  19135  psgneu  19607  odbezout  19659  sylow2blem3  19723  nn0gsumfz  20085  irredrmul  20542  zrninitoringc  20812  lbsextlem2  21320  znunit  21750  mptcoe1fsupp  22412  evls1fpws  22566  scmate  22704  scmatscm  22707  scmatfo  22724  mat1scmat  22733  pmatcoe1fsupp  22895  pmatcollpwfi  22976  pmatcollpw3fi  22979  mptcoe1matfsupp  22996  pm2mp  23019  chmaidscmat  23042  cpmadumatpoly  23077  chcoeffeq  23080  cayhamlem3  23081  cayhamlem4  23082  neiptopnei  23326  neitr  23374  cnpnei  23458  haust1  23546  isnrm3  23553  isreg2  23571  tgcmp  23595  hauscmplem  23600  hauscmp  23601  bwth  23604  1stcfb  23639  1stcelcls  23655  lly1stc  23690  txcmplem1  23835  txlm  23842  xkococnlem  23853  filuni  24079  filufint  24114  ufilen  24124  fclscf  24219  cnextcn  24261  ustex2sym  24411  ustex3sym  24412  utopreg  24446  isucn2  24472  ucnima  24474  ucncn  24478  neipcfilu  24489  metequiv2  24704  metrest  24718  xrsmopn  25007  mulc1cncf  25101  cncfco  25103  bndth  25154  lmmcvg  25457  cfil3i  25465  iscau4  25475  cmetcaulem  25484  iscmet3lem1  25487  caussi  25493  equivcfil  25495  equivcau  25496  caubl  25504  minveclem3b  25624  ovolgelb  25676  ovollb2lem  25684  ovolctb  25686  ovolicc2lem4  25716  ioombl1lem4  25757  dyadmax  25794  volsup2  25801  itg2monolem1  25946  c1liplem1  26192  c1lip1  26193  dvivthlem1  26204  lhop1  26210  ftc1a  26233  ftc1lem6  26237  ply1divex  26331  elply2  26390  dgrlem  26423  aacjcl  26527  aalioulem2  26533  aalioulem3  26534  aalioulem4  26535  ulmcaulem  26594  ulmcau  26595  ulmss  26597  mtest  26604  itgulm  26608  reeff1o  26647  efif1olem4  26747  rlimcnp  27167  xrlimcnp  27170  lgamucov  27239  ftalem3  27276  fta  27281  muval1  27334  dvdssqf  27339  mumullem1  27380  lgsqrmod  27553  lgsqrmodndvds  27554  pntlem3  27810  ostth  27840  nosupno  27904  nosupbnd1lem4  27912  noinfno  27919  noinfbnd1lem4  27927  conway  28009  etaslts  28023  znegscl  28622  tgtrisegint  28805  tgbtwndiff  28812  tgcgrxfr  28824  lnext  28873  legov2  28892  legtrd  28895  hlcgrex  28925  colperpexlem3  29050  colperpex  29051  hlpasch  29075  hpgerlem  29084  hpgtr  29087  dfcgra2  29178  acopy  29181  inagswap  29195  inaghl  29199  cgrg3col4  29207  axpasch  29328  wwlksnredwwlkn0  30282  midwwlks2s3  30338  clwwlkn1loopb  30431  2pthfrgrrn2  30671  frgrwopreg1  30706  frgrwopreg2  30707  grpoidinvlem3  30895  grpoideu  30898  grpoinveu  30908  ubthlem1  31259  minvecolem5  31270  htthlem  31306  chscllem2  32027  nmopun  32403  lnconi  32422  rnbra  32496  sumdmdii  32804  cdj3lem2b  32826  foresf1o  32887  acunirnmpt  33041  xrofsup  33149  fprodex01  33206  mndlactfo  33378  mndractfo  33380  isarchi3  33538  isarchiofld  33550  erler  33616  erld2  33617  dfufd2lem  33870  constrconj  34166  constrextdg2lem  34169  constrcjcl  34189  lmxrge0  34373  lmdvg  34374  esumlub  34481  esumfsup  34491  esumcvg  34507  ftc2re  35017  cusgr3cyclex  35649  cvmliftmolem2  35795  cvmlift2lem12  35827  satfv1  35876  satffunlem1lem2  35916  satffunlem2lem2  35919  satfv0fvfmla0  35926  ellcsrspsn  36154  r1peuqusdeg1  36156  wzel  36335  wsuclem  36336  btwndiff  36540  trisegint  36541  cgrxfr  36568  lineext  36589  segcon2  36618  brsegle2  36622  seglecgr12im  36623  segletr  36627  broutsideof3  36639  opnrebl2  36873  nn0prpw  36875  fin2so  38299  poimirlem27  38339  poimirlem30  38342  poimirlem31  38343  poimir  38345  mblfinlem1  38349  mblfinlem2  38350  mblfinlem3  38351  mblfinlem4  38352  itg2addnclem  38363  ftc1cnnc  38384  ftc1anclem5  38389  sdclem1  38435  geomcau  38451  equivtotbnd  38470  bndss  38478  ismtybndlem  38498  heibor1lem  38501  rrncmslem  38524  rngo2  38599  prtlem15  39690  lsateln0  39810  lsat0cv  39848  eqlkr3  39916  lkrshp  39920  lshpset2N  39934  hlhgt2  40204  hlrelat2  40218  atle  40251  athgt  40271  2dim  40285  1cvratex  40288  ps-2  40293  dalem20  40508  lhpexle1lem  40822  lhpexle1  40823  lhpexle2lem  40824  lhpmcvr5N  40842  lhpmcvr6N  40843  cdleme25a  41168  cdleme29ex  41189  cdlemfnid  41379  cdlemg33b0  41516  cdlemg33a  41521  cdlemg35  41528  cdleml3N  41793  dihlsscpre  42049  dih1dimb2  42056  dihatexv  42153  dvh3dim2  42263  dochkr1  42293  dochkr1OLDN  42294  lcfl8  42317  lcfl8b  42319  lcfrlem5  42361  lcfrlem6  42362  mapdrvallem2  42460  mapdh9a  42604  mapdh9aOLDN  42605  hdmaprnlem3eN  42673  hdmaprnlem16N  42677  mndmolinv  42903  primrootsunit1  42905  flt4lem5elem  43424  flt4lem7  43432  nna4b4nsq  43433  fphpdo  43585  rencldnfilem  43588  irrapxlem2  43591  oasubex  44054  tfsconcatlem  44104  tfsconcatrev  44116  cvgdvgrat  45064  expgrowth  45086  projf1o  45955  ssfiunibd  46069  supxrgere  46090  supxrgelem  46094  suplesup  46096  infrpge  46108  infleinf  46128  supxrunb3  46155  unb2ltle  46170  uzub  46186  cvgcaule  46246  qinioo  46292  qelioo  46303  climinf  46363  mullimc  46373  islptre  46376  limccog  46377  mullimcf  46380  limcrecl  46386  sumnnodd  46387  neglimc  46402  0ellimcdiv  46404  limclner  46406  allbutfifvre  46430  climleltrp  46431  fnlimabslt  46434  climinf2lem  46461  limsuppnflem  46465  limsupvaluz2  46493  supcnvlimsup  46495  limsupgtlem  46532  liminflelimsupuz  46540  liminflimsupclim  46562  limsupub2  46567  xlimpnfxnegmnf  46569  cncfioobd  46652  stoweidlem7  46762  stoweidlem27  46782  stoweidlem39  46794  stoweidlem48  46803  stoweidlem49  46804  stoweidlem60  46815  stoweidlem61  46816  stoweid  46818  dirkercncflem2  46859  fourierdlem20  46882  fourierdlem39  46901  fourierdlem41  46903  fourierdlem48  46909  fourierdlem49  46910  fourierdlem50  46911  fourierdlem64  46925  fourierdlem73  46934  fourierdlem74  46935  fourierdlem75  46936  fourierdlem87  46948  fourierdlem103  46964  fourierdlem104  46965  qndenserrnopnlem  47052  sge0ltfirp  47155  sge0gerpmpt  47157  sge0ltfirpmpt2  47181  sge0isum  47182  sge0pnffigtmpt  47195  sge0pnffsumgt  47197  sge0gtfsumgt  47198  sge0uzfsumgt  47199  nnfoctbdjlem  47210  meaiuninclem  47235  meaiuninc3v  47239  omeiunltfirp  47274  carageniuncllem2  47277  volicorescl  47308  hoidmv1le  47349  hoidmvlelem3  47352  hoiqssbllem3  47379  hspmbllem2  47382  iunhoiioolem  47430  vonioo  47437  vonicc  47440  smfaddlem1  47518  smflimlem2  47527  smflimlem3  47528  smfmullem4  47549  fsetsnfo  47831  2reu8i  47891  imasetpreimafvbijlemfo  48195  2pwp1prmfmtno  48383  proththd  48407  sbgoldbwt  48583  sbgoldbst  48584  sbgoldbalt  48587  bgoldbtbndlem4  48614  bgoldbtbnd  48615  grtriprop  48747  ply1mulgsumlem3  49209  ply1mulgsumlem4  49210  islindeps2  49304  isldepslvec2  49306