Theorem reximdv 2645

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 2644	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2205  ∃wrex 2523

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527  df-rex 2528

This theorem is referenced by:  r19.12  2651  reusv3  4586  rexxfrd  4589  iunpw  4606  fvelima  5733  carden2bex  7499  prnmaddl  7821  prarloclem5  7831  prarloc2  7835  genprndl  7852  genprndu  7853  ltpopr  7926  recexprlemm  7955  recexprlemopl  7956  recexprlemopu  7958  recexprlem1ssl  7964  recexprlem1ssu  7965  cauappcvgprlemupu  7980  caucvgprlemupu  8003  caucvgprprlemupu  8031  caucvgsrlemoffres  8131  map2psrprg  8136  resqrexlemgt0  11730  subcn2  12021  bezoutlembz  12725  pythagtriplem19  13005  mplsubgfileminv  14981  tgcl  15055  neiss  15141  ssnei2  15148  tgcnp  15200  cnptopco  15213  cnptopresti  15229  lmtopcnp  15241  blssexps  15420  blssex  15421  mopni3  15475  neibl  15482  metss  15485  metcnp3  15502  mpomulcn  15557  rescncf  15572  limcresi  15657  plyss  15729  umgrnloop0  16238  uhgr2edg  16327