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

Theorem reximdai 3253
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 3249 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 3082 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1778  wcel 2099  wral 3056  wrex 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2164
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-nf 1779  df-ral 3057  df-rex 3066
This theorem is referenced by:  2reurex  3753  fompt  7122  tz7.49  8459  hsmexlem2  10444  acunirnmpt2  32439  acunirnmpt2f  32440  locfinreflem  33431  cmpcref  33441  fvineqsneq  36881  indexdom  37196  filbcmb  37202  cdlemefr29exN  39864  rexanuz3  44434  reximdd  44490  disjrnmpt2  44533  disjinfi  44537  iunmapsn  44562  infnsuprnmpt  44598  rnmptbdlem  44603  supxrge  44692  suplesup  44693  infxr  44721  allbutfi  44747  supxrunb3  44753  infxrunb3rnmpt  44782  infrpgernmpt  44819  limsupre  45001  limsupub  45064  limsupre3lem  45092  limsupgtlem  45137  xlimmnfvlem1  45192  xlimpnfvlem1  45196  stoweidlem31  45391  stoweidlem34  45394  fourierdlem73  45539  sge0pnffigt  45756  sge0ltfirp  45760  sge0reuzb  45808  iundjiun  45820  ovnlerp  45922  smflimlem4  46134  smflimsuplem7  46186
  Copyright terms: Public domain W3C validator