Theorem eximdv 1916

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1832. See eximdh 1863 and eximd 2217 for versions without a distinct variable condition. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
alimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
eximdv	⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem eximdv

Step	Hyp	Ref	Expression
1		ax-5 1909	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1863	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  2eximdv  1918  exlimdv  1932  19.41v  1949  equvinva  2029  dfmoeu  2539  moim  2547  mo4  2569  reximdv2  3170  cgsexg  3536  spcimdv  3606  spcegv  3610  euind  3746  sbcimdv  3878  reupick  4348  reximdva0  4378  uniss  4939  dfiun2g  5053  eusvnfb  5411  reusv2lem3  5418  axprlem1  5441  axprlem2  5442  axprlem3  5443  axpr  5446  exexneq  5454  relopabi  5846  coss1  5880  coss2  5881  ssrelrn  5919  dmss  5927  dmcosseq  5999  dmcosseqOLD  6000  funssres  6622  brprcneu  6910  brprcneuALT  6911  fv3  6938  dffv2  7017  fvn0ssdmfun  7108  dffo4  7137  dffo5  7138  funopsn  7182  fvclss  7278  fsnex  7319  f1prex  7320  f1eqcocnv  7337  mapsnd  8944  enp1iOLD  9342  en2  9343  en4  9345  marypha2  9508  brwdom3  9651  isinffi  10061  infpwfien  10131  infmap2  10286  cfub  10318  cflm  10319  cff1  10327  cfss  10334  isf32lem9  10430  axcc4  10508  acncc  10509  domtriomlem  10511  ac6s  10553  iundom2g  10609  winalim2  10765  grudomon  10886  nsmallnq  11046  prnmadd  11066  ltexprlem1  11105  ltexprlem3  11107  ltexprlem4  11108  reclem2pr  11117  dedekind  11453  xrsupsslem  13369  xrinfmsslem  13370  ishashinf  14512  hash3tpde  14542  coss12d  15021  supcvg  15904  vdwlem2  17029  ram0  17069  mreexexlem2d  17703  initoeu1  18078  termoeu1  18085  acsmapd  18624  acsmap2d  18625  dirge  18673  odcau  19646  ablfac2  20133  lspprat  21178  cmpsub  23429  cmpcld  23431  2ndcsep  23488  1stcelcls  23490  txcn  23655  fgcl  23907  ufildom1  23955  metustexhalf  24590  bcthlem5  25381  mbfi1flim  25778  itg2seq  25797  dchrisumlem3  27553  upgrex  29127  uhgrvd00  29570  wlkiswwlksupgr2  29910  wlklnwwlkln2lem  29915  umgrwwlks2on  29990  wpthswwlks2on  29994  frcond3  30301  frgrncvvdeqlem9  30339  ubthlem1  30902  axhcompl-zf  31030  isch3  31273  cnlnssadj  32112  acunirnmpt  32677  f1ocnt  32807  wrdpmtrlast  33086  qsxpid  33355  zarclsint  33818  insiga  34101  bnj605  34883  bnj607  34892  bnj1018g  34939  bnj1018  34940  cusgredgex  35089  loop1cycl  35105  erdsze2lem1  35171  fundmpss  35730  bj-zfauscl  36890  bj-restn0  37056  dissneqlem  37306  relowlpssretop  37330  pibt2  37383  poimirlem30  37610  fdc1  37706  prdstotbnd  37754  cossss  38381  prter2  38837  lsat0cv  38989  pmapglb2N  39728  elpaddn0  39757  cdlemftr3  40522  dibglbN  41123  dihglbcpreN  41257  dihjatcclem4  41378  mapdordlem2  41594  sticksstones3  42105  sticksstones20  42123  sn-axprlem3  42210  eu6w  42631  dfac11  43019  neik0pk1imk0  44009  rr-spce  44166  cpcolld  44227  ismnushort  44270  ax6e2ndeq  44530  fnchoice  44929  rfcnnnub  44936  eliin2f  45006  founiiun0  45097  disjinfi  45099  axccd  45136  axccd2  45137  fvelima2  45169  fzisoeu  45215  islpcn  45560  lptre2pt  45561  stoweidlem14  45935  stoweidlem35  45956  stoweidlem39  45960  stoweidlem50  45971  stoweidlem56  45977  stoweidlem59  45980  stoweidlem60  45981  fourier2  46148  qndenserrnbllem  46215  qndenserrn  46220  ovncvrrp  46485  ovnsubaddlem2  46492  hoidmvval0b  46511  hoiqssbllem3  46545  natlocalincr  46795  tworepnotupword  46805  funressnfv  46958  imasetpreimafvbijlemfv1  47277  fundcmpsurinjpreimafv  47282  elsprel  47349  grilcbri2  47828  subthinc  48707