MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximdai Structured version   Visualization version   GIF version

Theorem reximdai 2995
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
Hypotheses
Ref Expression
reximdai.1 𝑥𝜑
reximdai.2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
Assertion
Ref Expression
reximdai (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))

Proof of Theorem reximdai
StepHypRef Expression
1 reximdai.1 . . 3 𝑥𝜑
2 reximdai.2 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
31, 2ralrimi 2940 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 2991 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1699  wcel 1977  wral 2896  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902
This theorem is referenced by:  tz7.49  7427  hsmexlem2  9132  acunirnmpt2  28842  acunirnmpt2f  28843  locfinreflem  29235  cmpcref  29245  indexdom  32699  filbcmb  32705  cdlemefr29exN  34708  rexanuz3  38303  disjrnmpt2  38370  fompt  38374  disjinfi  38375  iunmapsn  38404  supxrge  38495  suplesup  38496  infxr  38524  allbutfi  38557  limsupre  38708  stoweidlem31  38924  stoweidlem34  38927  fourierdlem73  39072  sge0pnffigt  39289  sge0ltfirp  39293  sge0reuzb  39341  iundjiun  39353  ovnlerp  39452  smflimlem4  39660  2reurex  39830
  Copyright terms: Public domain W3C validator