Theorem reximdv 2633

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

Syntax hints:   → wi 4   ∈ wcel 2202  ∃wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  r19.12  2639  reusv3  4557  rexxfrd  4560  iunpw  4577  fvelima  5697  carden2bex  7394  prnmaddl  7710  prarloclem5  7720  prarloc2  7724  genprndl  7741  genprndu  7742  ltpopr  7815  recexprlemm  7844  recexprlemopl  7845  recexprlemopu  7847  recexprlem1ssl  7853  recexprlem1ssu  7854  cauappcvgprlemupu  7869  caucvgprlemupu  7892  caucvgprprlemupu  7920  caucvgsrlemoffres  8020  map2psrprg  8025  resqrexlemgt0  11585  subcn2  11876  bezoutlembz  12580  pythagtriplem19  12860  mplsubgfileminv  14720  tgcl  14794  neiss  14880  ssnei2  14887  tgcnp  14939  cnptopco  14952  cnptopresti  14968  lmtopcnp  14980  blssexps  15159  blssex  15160  mopni3  15214  neibl  15221  metss  15224  metcnp3  15241  mpomulcn  15296  rescncf  15311  limcresi  15396  plyss  15468  umgrnloop0  15974  uhgr2edg  16063