Theorem reximdva 3204

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
reximdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		reximdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 412	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 3201	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-rex 3071

This theorem is referenced by:  reximddv  3205  reximdvva  3207  reximddv2  3208  wereu2  5585  frpomin  6240  dffo4  6973  nnaordex  8445  frfi  9020  fisupg  9023  marypha1  9154  fiinfg  9219  wemapsolem  9270  unwdomg  9304  frminOLD  9491  rankr1ai  9540  cofsmo  10009  cfcoflem  10012  inar1  10515  nqerf  10670  prlem936  10787  fimaxre  11902  fiminre  11905  arch  12213  bndndx  12215  suprfinzcl  12418  zmin  12666  elpq  12697  qbtwnxr  12916  qsqueeze  12917  qextltlem  12918  xrsupsslem  13023  xrinfmsslem  13024  xrub  13028  supxrunb1  13035  ssnn0fi  13686  fsuppmapnn0fiub0  13694  fsuppmapnn0fz  13697  expnlbnd2  13930  r19.29uz  15043  cau3lem  15047  rlim2lt  15187  rlimclim  15236  2clim  15262  o1co  15276  climcn1  15282  climcn2  15283  rlimo1  15307  climsqz  15331  climsqz2  15332  rlimsqzlem  15341  lo1le  15344  climsup  15362  climcau  15363  caucvgrlem2  15367  iseralt  15377  cvgcmp  15509  cvgcmpce  15511  supcvg  15549  rpnnen2lem12  15915  bezoutlem1  16228  divgcdcoprmex  16352  exprmfct  16390  prmdvdsfz  16391  prmdvdsncoprmbd  16412  pclem  16520  pc2dvds  16561  pcprmpw  16565  dvdsprmpweqle  16568  unbenlem  16590  infpnlem2  16593  infpn2  16595  prmunb  16596  vdwlem2  16664  ramub1lem2  16709  prmdvdsprmop  16725  prmgaplem7  16739  ipodrsima  18240  smndex1mgm  18527  grpinveu  18595  dfgrp3lem  18654  psgneu  19095  odbezout  19146  sylow2blem3  19208  nn0gsumfz  19566  ringadd2  19795  irredrmul  19930  lbsextlem2  20402  znunit  20752  mptcoe1fsupp  21367  scmate  21640  scmatscm  21643  scmatfo  21660  mat1scmat  21669  pmatcoe1fsupp  21831  pmatcollpwfi  21912  pmatcollpw3fi  21915  mptcoe1matfsupp  21932  pm2mp  21955  chmaidscmat  21978  cpmadumatpoly  22013  chcoeffeq  22016  cayhamlem3  22017  cayhamlem4  22018  neiptopnei  22264  neitr  22312  cnpnei  22396  haust1  22484  isnrm3  22491  isreg2  22509  tgcmp  22533  hauscmplem  22538  hauscmp  22539  bwth  22542  1stcfb  22577  1stcelcls  22593  lly1stc  22628  txcmplem1  22773  txlm  22780  xkococnlem  22791  filuni  23017  filufint  23052  ufilen  23062  fclscf  23157  cnextcn  23199  ustex2sym  23349  ustex3sym  23350  utopreg  23385  isucn2  23412  ucnima  23414  ucncn  23418  neipcfilu  23429  metequiv2  23647  metrest  23661  xrsmopn  23956  mulc1cncf  24049  cncfco  24051  bndth  24102  lmmcvg  24406  cfil3i  24414  iscau4  24424  cmetcaulem  24433  iscmet3lem1  24436  caussi  24442  equivcfil  24444  equivcau  24445  caubl  24453  minveclem3b  24573  ovolgelb  24625  ovollb2lem  24633  ovolctb  24635  ovolicc2lem4  24665  ioombl1lem4  24706  dyadmax  24743  volsup2  24750  itg2monolem1  24896  c1liplem1  25141  c1lip1  25142  dvivthlem1  25153  lhop1  25159  ftc1a  25182  ftc1lem6  25186  ply1divex  25282  elply2  25338  dgrlem  25371  aacjcl  25468  aalioulem2  25474  aalioulem3  25475  aalioulem4  25476  ulmcaulem  25534  ulmcau  25535  ulmss  25537  mtest  25544  itgulm  25548  reeff1o  25587  efif1olem4  25682  rlimcnp  26096  xrlimcnp  26099  lgamucov  26168  ftalem3  26205  fta  26210  muval1  26263  dvdssqf  26268  mumullem1  26309  lgsqrmod  26481  lgsqrmodndvds  26482  pntlem3  26738  ostth  26768  tgtrisegint  26841  tgbtwndiff  26848  tgcgrxfr  26860  lnext  26909  legov2  26928  legtrd  26931  hlcgrex  26958  colperpexlem3  27074  colperpex  27075  hlpasch  27098  hpgerlem  27107  hpgtr  27110  dfcgra2  27172  acopy  27175  inagswap  27183  inaghl  27187  cgrg3col4  27195  axpasch  27290  wwlksnredwwlkn0  28240  midwwlks2s3  28296  clwwlkn1loopb  28386  2pthfrgrrn2  28626  frgrwopreg1  28661  frgrwopreg2  28662  grpoidinvlem3  28847  grpoideu  28850  grpoinveu  28860  ubthlem1  29211  minvecolem5  29222  htthlem  29258  chscllem2  29979  nmopun  30355  lnconi  30374  rnbra  30448  sumdmdii  30756  cdj3lem2b  30778  foresf1o  30829  acunirnmpt  30975  xrofsup  31069  fprodex01  31118  isarchi3  31420  isarchiofld  31495  lmxrge0  31881  lmdvg  31882  esumlub  32007  esumfsup  32017  esumcvg  32033  ftc2re  32557  cusgr3cyclex  33077  cvmliftmolem2  33223  cvmlift2lem12  33255  satfv1  33304  satffunlem1lem2  33344  satffunlem2lem2  33347  satfv0fvfmla0  33354  wzel  33797  wsuclem  33798  nosupno  33885  nosupbnd1lem4  33893  noinfno  33900  noinfbnd1lem4  33908  conway  33972  etasslt  33986  btwndiff  34308  trisegint  34309  cgrxfr  34336  lineext  34357  segcon2  34386  brsegle2  34390  seglecgr12im  34391  segletr  34395  broutsideof3  34407  opnrebl2  34489  nn0prpw  34491  fin2so  35743  poimirlem27  35783  poimirlem30  35786  poimirlem31  35787  poimir  35789  mblfinlem1  35793  mblfinlem2  35794  mblfinlem3  35795  mblfinlem4  35796  itg2addnclem  35807  ftc1cnnc  35828  ftc1anclem5  35833  sdclem1  35880  geomcau  35896  equivtotbnd  35915  bndss  35923  ismtybndlem  35943  heibor1lem  35946  rrncmslem  35969  rngo2  36044  prtlem15  36868  lsateln0  36988  lsat0cv  37026  eqlkr3  37094  lkrshp  37098  lshpset2N  37112  hlhgt2  37382  hlrelat2  37396  atle  37429  athgt  37449  2dim  37463  1cvratex  37466  ps-2  37471  dalem20  37686  lhpexle1lem  38000  lhpexle1  38001  lhpexle2lem  38002  lhpmcvr5N  38020  lhpmcvr6N  38021  cdleme25a  38346  cdleme29ex  38367  cdlemfnid  38557  cdlemg33b0  38694  cdlemg33a  38699  cdlemg35  38706  cdleml3N  38971  dihlsscpre  39227  dih1dimb2  39234  dihatexv  39331  dvh3dim2  39441  dochkr1  39471  dochkr1OLDN  39472  lcfl8  39495  lcfl8b  39497  lcfrlem5  39539  lcfrlem6  39540  mapdrvallem2  39638  mapdh9a  39782  mapdh9aOLDN  39783  hdmaprnlem3eN  39851  hdmaprnlem16N  39855  flt4lem5elem  40468  flt4lem7  40476  nna4b4nsq  40477  fphpdo  40619  rencldnfilem  40622  irrapxlem2  40625  cvgdvgrat  41884  expgrowth  41906  projf1o  42689  ssfiunibd  42802  supxrgere  42826  supxrgelem  42830  suplesup  42832  infrpge  42844  infleinf  42865  supxrunb3  42893  unb2ltle  42909  uzub  42925  qinioo  43027  qelioo  43038  climinf  43101  mullimc  43111  islptre  43114  limccog  43115  mullimcf  43118  limcrecl  43124  sumnnodd  43125  neglimc  43142  0ellimcdiv  43144  limclner  43146  allbutfifvre  43170  climleltrp  43171  fnlimabslt  43174  climinf2lem  43201  limsuppnflem  43205  limsupvaluz2  43233  supcnvlimsup  43235  limsupgtlem  43272  liminflelimsupuz  43280  liminflimsupclim  43302  limsupub2  43307  xlimpnfxnegmnf  43309  cncfioobd  43392  stoweidlem7  43502  stoweidlem27  43522  stoweidlem39  43534  stoweidlem48  43543  stoweidlem49  43544  stoweidlem60  43555  stoweidlem61  43556  stoweid  43558  dirkercncflem2  43599  fourierdlem20  43622  fourierdlem39  43641  fourierdlem41  43643  fourierdlem48  43649  fourierdlem49  43650  fourierdlem50  43651  fourierdlem64  43665  fourierdlem73  43674  fourierdlem74  43675  fourierdlem75  43676  fourierdlem87  43688  fourierdlem103  43704  fourierdlem104  43705  qndenserrnopnlem  43792  sge0ltfirp  43892  sge0gerpmpt  43894  sge0ltfirpmpt2  43918  sge0isum  43919  sge0pnffigtmpt  43932  sge0pnffsumgt  43934  sge0gtfsumgt  43935  sge0uzfsumgt  43936  nnfoctbdjlem  43947  meaiuninclem  43972  meaiuninc3v  43976  omeiunltfirp  44011  carageniuncllem2  44014  hoicvr  44040  volicorescl  44045  hoidmv1le  44086  hoidmvlelem3  44089  hoiqssbllem3  44116  hspmbllem2  44119  iunhoiioolem  44167  vonioo  44174  vonicc  44177  smfaddlem1  44249  smflimlem2  44258  smflimlem3  44259  smfmullem4  44279  fsetsnfo  44498  2reu8i  44556  imasetpreimafvbijlemfo  44809  2pwp1prmfmtno  44994  proththd  45018  sbgoldbwt  45181  sbgoldbst  45182  sbgoldbalt  45185  bgoldbtbndlem4  45212  bgoldbtbnd  45213  zrninitoringc  45581  ply1mulgsumlem3  45681  ply1mulgsumlem4  45682  islindeps2  45776  isldepslvec2  45778