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

Theorem r19.29a 3072
 Description: A commonly used pattern based on r19.29 3066. (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 1840 . 2 𝑥𝜑
2 r19.29a.1 . 2 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
3 r19.29a.2 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
41, 2, 3r19.29af 3070 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1987  ∃wrex 2908 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-ral 2912  df-rex 2913 This theorem is referenced by:  xpdifid  5526  modmuladdnn0  12661  1arith  15562  prmgaplem5  15690  prmgapprmolem  15696  ffthiso  16517  mhmid  17464  mhmmnd  17465  ghmgrp  17467  ghmcmn  18165  ablfac2  18416  zringlpirlem1  19760  mp2pm2mplem4  20542  neiptopuni  20853  neiptoptop  20854  neiptopnei  20855  neitr  20903  hauscmplem  21128  2ndcomap  21180  lly1stc  21218  dissnref  21250  neitx  21329  cnextcn  21790  ustexsym  21938  ustex2sym  21939  ustex3sym  21940  trust  21952  utoptop  21957  restutop  21960  restutopopn  21961  ustuqtop1  21964  ustuqtop2  21965  ustuqtop3  21966  ustuqtop4  21967  utopreg  21975  ucncn  22008  fmucnd  22015  cfilufg  22016  trcfilu  22017  neipcfilu  22019  metustid  22278  metustsym  22279  metustexhalf  22280  metust  22282  cfilucfil  22283  metustbl  22290  psmetutop  22291  restmetu  22294  qdensere  22492  opnreen  22553  nmoleub2lem3  22834  ovolicc2lem4  23207  plydivlem4  23968  ulmuni  24063  dchrpt  24905  tgcgrtriv  25292  tgbtwntriv2  25295  tgbtwncom  25296  tgbtwnswapid  25300  tgbtwnintr  25301  tgbtwnouttr2  25303  tgtrisegint  25307  tgifscgr  25316  tgcgrxfr  25326  tgbtwnxfr  25338  motcgrg  25352  tgbtwnconn1lem3  25382  tgbtwnconn1  25383  tgbtwnconn3  25385  legval  25392  legov  25393  legov2  25394  legtrd  25397  legtri3  25398  legtrid  25399  ltgseg  25404  hlcgrex  25424  hlcgreulem  25425  colline  25457  miriso  25478  symquadlem  25497  krippenlem  25498  midexlem  25500  perpneq  25522  isperp2  25523  footex  25526  perpdrag  25533  colperpexlem3  25537  colperpex  25538  opphllem  25540  mideulem  25541  midex  25542  oppne3  25548  oppnid  25551  opphllem3  25554  opphllem5  25556  opphllem6  25557  oppperpex  25558  opphl  25559  outpasch  25560  hpgne1  25566  hpgne2  25567  lnopp2hpgb  25568  colopp  25574  lmieu  25589  lnperpex  25608  trgcopy  25609  trgcopyeulem  25610  acopy  25637  acopyeu  25638  inaghl  25644  cgrg3col4  25647  tgasa1  25652  f1otrg  25664  ttgbtwnid  25677  cnvbraval  28836  opsqrlem1  28866  rabfodom  29209  acunirnmpt  29319  acunirnmpt2  29320  acunirnmpt2f  29321  xrge0infss  29387  archirngz  29546  archiabllem1a  29548  archiabllem1b  29549  archiabllem1  29550  archiabllem2a  29551  archiabllem2c  29552  archiabl  29555  gsummpt2d  29584  fimaproj  29700  txomap  29701  qtophaus  29703  pcmplfinf  29728  pstmxmet  29740  pnfneige0  29797  esumcst  29924  esum2d  29954  esumiun  29955  ddemeas  30098  signsply0  30426  signstres  30450  poimirlem17  33085  poimirlem20  33088  itg2gt0cn  33124  fdc1  33201  lhprelat3N  34833  dihjat2  36227  eldioph2b  36833  diophrex  36846  irrapxlem6  36898  pellex  36906  pellfundex  36957  lnrfg  37197  mpaaeu  37228  cvgdvgrat  38021  climsuse  39267  limsupre  39300  limcleqr  39303  cncficcgt0  39427  dvbdfbdioo  39473  ioodvbdlimc1lem2  39475  ioodvbdlimc2lem  39477  stoweidlem28  39573  stoweidlem29  39574  stoweidlem52  39597  stoweidlem60  39605  fourierdlem39  39691  fourierdlem102  39753  fourierdlem103  39754  fourierdlem104  39755  fourierdlem114  39765  hspmbllem2  40169  nnsum4primesevenALTV  40999
 Copyright terms: Public domain W3C validator