Theorem r19.29a 3060

Description: A commonly used pattern based on r19.29 3054. (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

Step	Hyp	Ref	Expression
1		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜑
2		r19.29a.1	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
3		r19.29a.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
4	1, 2, 3	r19.29af 3058	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902

This theorem is referenced by:  xpdifid  5481  1arith  15469  prmgaplem5  15597  prmgapprmolem  15603  ffthiso  16412  mhmid  17359  mhmmnd  17360  ghmgrp  17362  ghmcmn  18060  ablfac2  18311  zringlpirlem1  19651  mp2pm2mplem4  20433  neiptopuni  20744  neiptoptop  20745  neiptopnei  20746  neitr  20794  hauscmplem  21019  2ndcomap  21071  lly1stc  21109  dissnref  21141  neitx  21220  cnextcn  21681  ustexsym  21829  ustex2sym  21830  ustex3sym  21831  trust  21843  utoptop  21848  restutop  21851  restutopopn  21852  ustuqtop1  21855  ustuqtop2  21856  ustuqtop3  21857  ustuqtop4  21858  utopreg  21866  ucncn  21899  fmucnd  21906  cfilufg  21907  trcfilu  21908  neipcfilu  21910  metustid  22169  metustsym  22170  metustexhalf  22171  metust  22173  cfilucfil  22174  metustbl  22181  psmetutop  22182  restmetu  22185  qdensere  22383  opnreen  22442  nmoleub2lem3  22723  ovolicc2lem4  23095  plydivlem4  23855  ulmuni  23950  dchrpt  24792  tgcgrtriv  25179  tgbtwntriv2  25182  tgbtwncom  25183  tgbtwnswapid  25187  tgbtwnintr  25188  tgbtwnouttr2  25190  tgtrisegint  25194  tgifscgr  25203  tgcgrxfr  25213  tgbtwnxfr  25225  motcgrg  25239  tgbtwnconn1lem3  25269  tgbtwnconn1  25270  tgbtwnconn3  25272  legval  25279  legov  25280  legov2  25281  legtrd  25284  legtri3  25285  legtrid  25286  ltgseg  25291  hlcgrex  25311  hlcgreulem  25312  colline  25344  miriso  25365  symquadlem  25384  krippenlem  25385  midexlem  25387  perpneq  25409  isperp2  25410  footex  25413  perpdrag  25420  colperpexlem3  25424  colperpex  25425  opphllem  25427  mideulem  25428  midex  25429  oppne3  25435  oppnid  25438  opphllem3  25441  opphllem5  25443  opphllem6  25444  oppperpex  25445  opphl  25446  outpasch  25447  hpgne1  25453  hpgne2  25454  lnopp2hpgb  25455  colopp  25461  lmieu  25476  lnperpex  25495  trgcopy  25496  trgcopyeulem  25497  acopy  25524  acopyeu  25525  inaghl  25531  cgrg3col4  25534  tgasa1  25539  f1otrg  25551  ttgbtwnid  25564  cnvbraval  28353  opsqrlem1  28383  rabfodom  28728  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  xrge0infss  28915  archirngz  29074  archiabllem1a  29076  archiabllem1b  29077  archiabllem1  29078  archiabllem2a  29079  archiabllem2c  29080  archiabl  29083  gsummpt2d  29112  fimaproj  29228  txomap  29229  qtophaus  29231  pcmplfinf  29256  pstmxmet  29268  pnfneige0  29325  esumcst  29452  esum2d  29482  esumiun  29483  ddemeas  29626  signsply0  29954  signstres  29978  poimirlem17  32596  poimirlem20  32599  itg2gt0cn  32635  fdc1  32712  lhprelat3N  34344  dihjat2  35738  eldioph2b  36344  diophrex  36357  irrapxlem6  36409  pellex  36417  pellfundex  36468  lnrfg  36708  mpaaeu  36739  cvgdvgrat  37534  climsuse  38675  limsupre  38708  limcleqr  38711  cncficcgt0  38774  dvbdfbdioo  38820  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem28  38921  stoweidlem29  38922  stoweidlem52  38945  stoweidlem60  38953  fourierdlem39  39039  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  hspmbllem2  39517  nnsum4primesevenALTV  40217