Theorem r19.29a 3226

Description: A commonly used pattern based on r19.29 3220. (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 1995	. 2 ⊢ Ⅎ𝑥𝜑
2		r19.29a.1	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
3		r19.29a.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
4	1, 2, 3	r19.29af 3224	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2145  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-ex 1853  df-nf 1858  df-ral 3066  df-rex 3067

This theorem is referenced by:  xpdifid  5703  modmuladdnn0  12922  1arith  15838  prmgaplem5  15966  prmgapprmolem  15972  ffthiso  16796  mhmid  17744  mhmmnd  17745  ghmgrp  17747  ghmcmn  18444  ablfac2  18696  zringlpirlem1  20047  mp2pm2mplem4  20834  neiptopuni  21155  neiptoptop  21156  neiptopnei  21157  neitr  21205  hauscmplem  21430  2ndcomap  21482  lly1stc  21520  dissnref  21552  neitx  21631  cnextcn  22091  ustexsym  22239  ustex2sym  22240  ustex3sym  22241  trust  22253  utoptop  22258  restutop  22261  restutopopn  22262  ustuqtop1  22265  ustuqtop2  22266  ustuqtop3  22267  ustuqtop4  22268  utopreg  22276  ucncn  22309  fmucnd  22316  cfilufg  22317  trcfilu  22318  neipcfilu  22320  metustid  22579  metustsym  22580  metustexhalf  22581  metust  22583  cfilucfil  22584  metustbl  22591  psmetutop  22592  restmetu  22595  qdensere  22793  opnreen  22854  nmoleub2lem3  23134  ovolicc2lem4  23508  plydivlem4  24271  ulmuni  24366  dchrpt  25213  tgcgrtriv  25600  tgbtwntriv2  25603  tgbtwncom  25604  tgbtwnswapid  25608  tgbtwnintr  25609  tgbtwnouttr2  25611  tgtrisegint  25615  tgifscgr  25624  tgcgrxfr  25634  tgbtwnxfr  25646  motcgrg  25660  tgbtwnconn1lem3  25690  tgbtwnconn1  25691  tgbtwnconn3  25693  legval  25700  legov  25701  legov2  25702  legtrd  25705  legtri3  25706  legtrid  25707  ltgseg  25712  hlcgrex  25732  hlcgreulem  25733  colline  25765  miriso  25786  symquadlem  25805  krippenlem  25806  midexlem  25808  perpneq  25830  isperp2  25831  footex  25834  perpdrag  25841  colperpexlem3  25845  colperpex  25846  opphllem  25848  mideulem  25849  midex  25850  oppne3  25856  oppnid  25859  opphllem3  25862  opphllem5  25864  opphllem6  25865  oppperpex  25866  opphl  25867  outpasch  25868  hpgne1  25874  hpgne2  25875  lnopp2hpgb  25876  colopp  25882  lmieu  25897  lnperpex  25916  trgcopy  25917  trgcopyeulem  25918  acopy  25945  acopyeu  25946  inaghl  25952  cgrg3col4  25955  tgasa1  25960  f1otrg  25972  ttgbtwnid  25985  cnvbraval  29309  opsqrlem1  29339  rabfodom  29682  acunirnmpt  29799  acunirnmpt2  29800  acunirnmpt2f  29801  xrge0infss  29865  fsumiunle  29915  archirngz  30083  archiabllem1a  30085  archiabllem1b  30086  archiabllem1  30087  archiabllem2a  30088  archiabllem2c  30089  archiabl  30092  gsummpt2d  30121  fimaproj  30240  txomap  30241  qtophaus  30243  pcmplfinf  30268  pstmxmet  30280  pnfneige0  30337  esumcst  30465  esum2d  30495  esumiun  30496  ddemeas  30639  signsply0  30968  signstres  30992  prodfzo03  31021  actfunsnf1o  31022  actfunsnrndisj  31023  tgoldbachgt  31081  poimirlem17  33759  poimirlem20  33762  itg2gt0cn  33797  fdc1  33874  lhprelat3N  35848  dihjat2  37241  eldioph2b  37852  diophrex  37865  irrapxlem6  37917  pellex  37925  pellfundex  37976  lnrfg  38215  mpaaeu  38246  cvgdvgrat  39038  climsuse  40358  limsupre  40391  limcleqr  40394  xlimclim2lem  40583  climxlim2  40590  cncficcgt0  40619  dvbdfbdioo  40663  ioodvbdlimc1lem2  40665  ioodvbdlimc2lem  40667  stoweidlem28  40762  stoweidlem29  40763  stoweidlem52  40786  stoweidlem60  40794  fourierdlem39  40880  fourierdlem102  40942  fourierdlem103  40943  fourierdlem104  40944  fourierdlem114  40954  hspmbllem2  41361  nnsum4primesevenALTV  42217