Theorem reximdv 2631

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)

Hypothesis

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

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		reximdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	reximdvai 2630	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2200  ∃wrex 2509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  r19.12  2637  reusv3  4555  rexxfrd  4558  iunpw  4575  fvelima  5693  carden2bex  7385  prnmaddl  7700  prarloclem5  7710  prarloc2  7714  genprndl  7731  genprndu  7732  ltpopr  7805  recexprlemm  7834  recexprlemopl  7835  recexprlemopu  7837  recexprlem1ssl  7843  recexprlem1ssu  7844  cauappcvgprlemupu  7859  caucvgprlemupu  7882  caucvgprprlemupu  7910  caucvgsrlemoffres  8010  map2psrprg  8015  resqrexlemgt0  11571  subcn2  11862  bezoutlembz  12565  pythagtriplem19  12845  mplsubgfileminv  14704  tgcl  14778  neiss  14864  ssnei2  14871  tgcnp  14923  cnptopco  14936  cnptopresti  14952  lmtopcnp  14964  blssexps  15143  blssex  15144  mopni3  15198  neibl  15205  metss  15208  metcnp3  15225  mpomulcn  15280  rescncf  15295  limcresi  15380  plyss  15452  umgrnloop0  15958  uhgr2edg  16045