Theorem reximdv 2578

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

Syntax hints:   → wi 4   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  r19.12  2583  reusv3  4462  rexxfrd  4465  iunpw  4482  fvelima  5569  carden2bex  7190  prnmaddl  7491  prarloclem5  7501  prarloc2  7505  genprndl  7522  genprndu  7523  ltpopr  7596  recexprlemm  7625  recexprlemopl  7626  recexprlemopu  7628  recexprlem1ssl  7634  recexprlem1ssu  7635  cauappcvgprlemupu  7650  caucvgprlemupu  7673  caucvgprprlemupu  7701  caucvgsrlemoffres  7801  map2psrprg  7806  resqrexlemgt0  11031  subcn2  11321  bezoutlembz  12007  pythagtriplem19  12284  tgcl  13603  neiss  13689  ssnei2  13696  tgcnp  13748  cnptopco  13761  cnptopresti  13777  lmtopcnp  13789  blssexps  13968  blssex  13969  mopni3  14023  neibl  14030  metss  14033  metcnp3  14050  rescncf  14107  limcresi  14174