MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximddv Structured version   Unicode version

Theorem reximddv 2834
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)
Hypotheses
Ref Expression
reximddva.1  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
reximddva.2  |-  ( ph  ->  E. x  e.  A  ps )
Assertion
Ref Expression
reximddv  |-  ( ph  ->  E. x  e.  A  ch )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem reximddv
StepHypRef Expression
1 reximddva.2 . 2  |-  ( ph  ->  E. x  e.  A  ps )
2 reximddva.1 . . . 4  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
32expr 618 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
43reximdva 2833 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
51, 4mpd 15 1  |-  ( ph  ->  E. x  e.  A  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872   E.wrex 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-ral 2713  df-rex 2714
This theorem is referenced by:  reximddv2  2835  dedekind  9741  caucvgrlem  13672  caucvgrlemOLD  13673  isprm5  14587  drsdirfi  16119  sylow2  17214  gexex  17427  nrmsep  20308  regsep2  20327  locfincmp  20476  dissnref  20478  met1stc  21471  xrge0tsms  21787  cnheibor  21918  lmcau  22217  ismbf3d  22545  ulmdvlem3  23292  legov  24565  legtrid  24571  midexlem  24672  opphllem  24712  mideulem  24713  midex  24714  oppperpex  24730  hpgid  24743  lnperpex  24780  trgcopy  24781  grpoidinv  25871  pjhthlem2  26980  mdsymlem3  27993  xrge0tsmsd  28493  ballotlemfc0  29270  ballotlemfcc  29271  cvmliftlem15  29966  lhpexle3lem  33482  lhpex2leN  33484  cdlemg1cex  34061  nacsfix  35460  unxpwdom3  35860  rfcnnnub  37267  stoweidlem27  37764
  Copyright terms: Public domain W3C validator