Theorem reximdv 2651

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  r19.12  2657  reusv3  4608  rexxfrd  4611  iunpw  4628  fvelima  5757  carden2bex  7541  prnmaddl  7863  prarloclem5  7873  prarloc2  7877  genprndl  7894  genprndu  7895  ltpopr  7968  recexprlemm  7997  recexprlemopl  7998  recexprlemopu  8000  recexprlem1ssl  8006  recexprlem1ssu  8007  cauappcvgprlemupu  8022  caucvgprlemupu  8045  caucvgprprlemupu  8073  caucvgsrlemoffres  8173  map2psrprg  8178  resqrexlemgt0  11807  subcn2  12101  bezoutlembz  12805  pythagtriplem19  13089  tgcl  15307  neiss  15393  ssnei2  15400  tgcnp  15452  cnptopco  15465  cnptopresti  15481  lmtopcnp  15493  blssexps  15672  blssex  15673  mopni3  15727  neibl  15734  metss  15737  metcnp3  15754  mpomulcn  15809  rescncf  15824  limcresi  15909  plyss  15981  umgrnloop0  16580  uhgr2edg  16669