Theorem reximdv 2608

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

Syntax hints:   → wi 4   ∈ wcel 2177  ∃wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  r19.12  2613  reusv3  4515  rexxfrd  4518  iunpw  4535  fvelima  5643  carden2bex  7312  prnmaddl  7623  prarloclem5  7633  prarloc2  7637  genprndl  7654  genprndu  7655  ltpopr  7728  recexprlemm  7757  recexprlemopl  7758  recexprlemopu  7760  recexprlem1ssl  7766  recexprlem1ssu  7767  cauappcvgprlemupu  7782  caucvgprlemupu  7805  caucvgprprlemupu  7833  caucvgsrlemoffres  7933  map2psrprg  7938  resqrexlemgt0  11406  subcn2  11697  bezoutlembz  12400  pythagtriplem19  12680  mplsubgfileminv  14537  tgcl  14611  neiss  14697  ssnei2  14704  tgcnp  14756  cnptopco  14769  cnptopresti  14785  lmtopcnp  14797  blssexps  14976  blssex  14977  mopni3  15031  neibl  15038  metss  15041  metcnp3  15058  mpomulcn  15113  rescncf  15128  limcresi  15213  plyss  15285