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 3107
Description: A commonly used pattern based on r19.29 3101. (Contributed by Thierry Arnoux, 22-Nov-2017.)
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 nfv 1883 . 2 𝑥𝜑
2 r19.29a.1 . 2 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
3 r19.29a.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
41, 2, 3r19.29af 3105 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-ral 2946  df-rex 2947
This theorem is referenced by:  xpdifid  5597  modmuladdnn0  12754  1arith  15678  prmgaplem5  15806  prmgapprmolem  15812  ffthiso  16636  mhmid  17583  mhmmnd  17584  ghmgrp  17586  ghmcmn  18283  ablfac2  18534  zringlpirlem1  19880  mp2pm2mplem4  20662  neiptopuni  20982  neiptoptop  20983  neiptopnei  20984  neitr  21032  hauscmplem  21257  2ndcomap  21309  lly1stc  21347  dissnref  21379  neitx  21458  cnextcn  21918  ustexsym  22066  ustex2sym  22067  ustex3sym  22068  trust  22080  utoptop  22085  restutop  22088  restutopopn  22089  ustuqtop1  22092  ustuqtop2  22093  ustuqtop3  22094  ustuqtop4  22095  utopreg  22103  ucncn  22136  fmucnd  22143  cfilufg  22144  trcfilu  22145  neipcfilu  22147  metustid  22406  metustsym  22407  metustexhalf  22408  metust  22410  cfilucfil  22411  metustbl  22418  psmetutop  22419  restmetu  22422  qdensere  22620  opnreen  22681  nmoleub2lem3  22961  ovolicc2lem4  23334  plydivlem4  24096  ulmuni  24191  dchrpt  25037  tgcgrtriv  25424  tgbtwntriv2  25427  tgbtwncom  25428  tgbtwnswapid  25432  tgbtwnintr  25433  tgbtwnouttr2  25435  tgtrisegint  25439  tgifscgr  25448  tgcgrxfr  25458  tgbtwnxfr  25470  motcgrg  25484  tgbtwnconn1lem3  25514  tgbtwnconn1  25515  tgbtwnconn3  25517  legval  25524  legov  25525  legov2  25526  legtrd  25529  legtri3  25530  legtrid  25531  ltgseg  25536  hlcgrex  25556  hlcgreulem  25557  colline  25589  miriso  25610  symquadlem  25629  krippenlem  25630  midexlem  25632  perpneq  25654  isperp2  25655  footex  25658  perpdrag  25665  colperpexlem3  25669  colperpex  25670  opphllem  25672  mideulem  25673  midex  25674  oppne3  25680  oppnid  25683  opphllem3  25686  opphllem5  25688  opphllem6  25689  oppperpex  25690  opphl  25691  outpasch  25692  hpgne1  25698  hpgne2  25699  lnopp2hpgb  25700  colopp  25706  lmieu  25721  lnperpex  25740  trgcopy  25741  trgcopyeulem  25742  acopy  25769  acopyeu  25770  inaghl  25776  cgrg3col4  25779  tgasa1  25784  f1otrg  25796  ttgbtwnid  25809  cnvbraval  29097  opsqrlem1  29127  rabfodom  29470  acunirnmpt  29587  acunirnmpt2  29588  acunirnmpt2f  29589  xrge0infss  29653  fsumiunle  29703  archirngz  29871  archiabllem1a  29873  archiabllem1b  29874  archiabllem1  29875  archiabllem2a  29876  archiabllem2c  29877  archiabl  29880  gsummpt2d  29909  fimaproj  30028  txomap  30029  qtophaus  30031  pcmplfinf  30056  pstmxmet  30068  pnfneige0  30125  esumcst  30253  esum2d  30283  esumiun  30284  ddemeas  30427  signsply0  30756  signstres  30780  prodfzo03  30809  actfunsnf1o  30810  actfunsnrndisj  30811  tgoldbachgt  30869  poimirlem17  33556  poimirlem20  33559  itg2gt0cn  33595  fdc1  33672  lhprelat3N  35644  dihjat2  37037  eldioph2b  37643  diophrex  37656  irrapxlem6  37708  pellex  37716  pellfundex  37767  lnrfg  38006  mpaaeu  38037  cvgdvgrat  38829  climsuse  40158  limsupre  40191  limcleqr  40194  xlimclim2lem  40383  climxlim2  40390  cncficcgt0  40419  dvbdfbdioo  40463  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem28  40563  stoweidlem29  40564  stoweidlem52  40587  stoweidlem60  40595  fourierdlem39  40681  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  hspmbllem2  41162  nnsum4primesevenALTV  42014
  Copyright terms: Public domain W3C validator