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

Theorem reximddv 2908
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 2907 . 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 1870   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787  df-rex 2788
This theorem is referenced by:  reximddv2  2909  dedekind  9796  caucvgrlem  13714  caucvgrlemOLD  13715  isprm5  14622  drsdirfi  16134  sylow2  17213  gexex  17426  nrmsep  20304  regsep2  20323  locfincmp  20472  dissnref  20474  met1stc  21467  xrge0tsms  21763  cnheibor  21879  lmcau  22175  ismbf3d  22487  ulmdvlem3  23222  legov  24490  legtrid  24496  midexlem  24594  opphllem  24634  mideulem  24635  midex  24636  oppperpex  24652  hpgid  24664  lnperpex  24701  trgcopy  24702  grpoidinv  25781  pjhthlem2  26880  mdsymlem3  27893  xrge0tsmsd  28387  ballotlemfc0  29151  ballotlemfcc  29152  cvmliftlem15  29809  lhpexle3lem  33288  lhpex2leN  33290  cdlemg1cex  33867  nacsfix  35266  unxpwdom3  35662  rfcnnnub  37000  stoweidlem27  37459
  Copyright terms: Public domain W3C validator