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

Theorem r19.29a 3156
Description: A commonly used pattern in the spirit of r19.29 3114. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)
Hypotheses
Ref Expression
r19.29a.1 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
r19.29a.2 (𝜑 → ∃𝑥𝐴 𝜓)
Assertion
Ref Expression
r19.29a (𝜑𝜒)
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.29a
StepHypRef Expression
1 r19.29a.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
2 r19.29a.1 . . 3 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
32rexlimdva2 3151 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3071
This theorem is referenced by:  xpdifid  6121  fimaproj  8068  modmuladdnn0  13826  1arith  16804  prmgaplem5  16932  prmgapprmolem  16938  ffthiso  17821  mhmid  18873  mhmmnd  18874  ghmgrp  18876  ghmcmn  19615  ablfac2  19873  ringinvnz1ne0  20021  zringlpirlem1  20899  mp2pm2mplem4  22174  neiptopuni  22497  neiptoptop  22498  neiptopnei  22499  neitr  22547  hauscmplem  22773  2ndcomap  22825  lly1stc  22863  dissnref  22895  neitx  22974  cnextcn  23434  ustexsym  23583  ustex2sym  23584  ustex3sym  23585  trust  23597  utoptop  23602  restutop  23605  restutopopn  23606  ustuqtop1  23609  ustuqtop2  23610  ustuqtop3  23611  ustuqtop4  23612  utopreg  23620  ucncn  23653  fmucnd  23660  cfilufg  23661  trcfilu  23662  neipcfilu  23664  metustid  23926  metustsym  23927  metustexhalf  23928  metust  23930  cfilucfil  23931  metustbl  23938  psmetutop  23939  restmetu  23942  qdensere  24149  opnreen  24210  nmoleub2lem3  24494  ovolicc2lem4  24900  plydivlem4  25672  ulmuni  25767  dchrpt  26631  tgcgrtriv  27468  tgbtwntriv2  27471  tgbtwncom  27472  tgbtwnswapid  27476  tgbtwnintr  27477  tgbtwnouttr2  27479  tgtrisegint  27483  tgifscgr  27492  tgcgrxfr  27502  tgbtwnxfr  27514  motcgrg  27528  tgbtwnconn1lem3  27558  tgbtwnconn1  27559  tgbtwnconn3  27561  legval  27568  legov  27569  legov2  27570  legtrd  27573  legtri3  27574  legtrid  27575  ltgseg  27580  hlcgrex  27600  hlcgreulem  27601  colline  27633  miriso  27654  symquadlem  27673  krippenlem  27674  midexlem  27676  perpneq  27698  isperp2  27699  footexALT  27702  footex  27705  perpdrag  27712  colperpexlem3  27716  colperpex  27717  opphllem  27719  mideulem  27720  midex  27721  oppne3  27727  oppnid  27730  opphllem3  27733  opphllem5  27735  opphllem6  27736  oppperpex  27737  opphl  27738  outpasch  27739  hpgne1  27745  hpgne2  27746  lnopp2hpgb  27747  colopp  27753  lmieu  27768  lnperpex  27787  trgcopy  27788  trgcopyeulem  27789  acopy  27817  acopyeu  27818  inaghl  27829  leagne1  27833  leagne2  27834  leagne3  27835  leagne4  27836  cgrg3col4  27837  tgasa1  27842  f1otrg  27855  ttgbtwnid  27874  cnvbraval  31094  opsqrlem1  31124  rabfodom  31475  acunirnmpt  31621  acunirnmpt2  31622  acunirnmpt2f  31623  xrge0infss  31712  fsumiunle  31774  wrdt2ind  31856  mgcf1o  31912  gsummpt2d  31940  trsp2cyc  32021  cycpmrn  32041  tocyccntz  32042  cyc3evpm  32048  cyc3genpm  32050  cycpmgcl  32051  cycpmconjslem2  32053  cyc3conja  32055  archirngz  32074  archiabllem1a  32076  archiabllem1b  32077  archiabllem1  32078  archiabllem2a  32079  archiabllem2c  32080  archiabl  32083  imaslmod  32192  znfermltl  32202  nsgqusf1olem1  32239  ghmqusker  32246  rhmimaidl  32254  isprmidlc  32268  qsidomlem2  32274  mxidlprm  32285  dimval  32355  dimvalfi  32356  lssdimle  32360  lbsdiflsp0  32378  dimkerim  32379  fedgmul  32383  extdg1id  32409  txomap  32472  qtophaus  32474  pcmplfinf  32499  zarcls1  32507  zarclsun  32508  zarclsint  32510  zarclssn  32511  zarcmplem  32519  rhmpreimacn  32523  pstmxmet  32535  pnfneige0  32589  esumcst  32719  esum2d  32749  esumiun  32750  ddemeas  32892  signsply0  33220  signstres  33244  prodfzo03  33273  actfunsnf1o  33274  actfunsnrndisj  33275  tgoldbachgt  33333  poimirlem17  36141  poimirlem20  36144  itg2gt0cn  36179  fdc1  36251  lhprelat3N  38549  dihjat2  39940  aks4d1p8  40590  prjspersym  40988  eldioph2b  41129  diophrex  41141  irrapxlem6  41193  pellex  41201  pellfundex  41252  lnrfg  41489  mpaaeu  41520  cvgdvgrat  42681  climsuse  43935  limsupre  43968  limcleqr  43971  limsuppnfdlem  44028  limsupub2  44139  xlimclim2lem  44166  climxlim2  44173  cncficcgt0  44215  dvbdfbdioo  44257  ioodvbdlimc1lem2  44259  ioodvbdlimc2lem  44261  stoweidlem28  44355  stoweidlem29  44356  stoweidlem52  44379  stoweidlem60  44387  fourierdlem39  44473  fourierdlem102  44535  fourierdlem103  44536  fourierdlem104  44537  fourierdlem114  44547  hspmbllem2  44954  nnsum4primesevenALTV  46079
  Copyright terms: Public domain W3C validator