Theorem r19.29a 3266

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2156  ∃wrex 3097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-12 2214

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-ex 1860  df-nf 1864  df-ral 3101  df-rex 3102

This theorem is referenced by:  xpdifid  5773  modmuladdnn0  12938  1arith  15848  prmgaplem5  15976  prmgapprmolem  15982  ffthiso  16793  mhmid  17741  mhmmnd  17742  ghmgrp  17744  ghmcmn  18438  ablfac2  18690  zringlpirlem1  20040  mp2pm2mplem4  20827  neiptopuni  21148  neiptoptop  21149  neiptopnei  21150  neitr  21198  hauscmplem  21423  2ndcomap  21475  lly1stc  21513  dissnref  21545  neitx  21624  cnextcn  22084  ustexsym  22232  ustex2sym  22233  ustex3sym  22234  trust  22246  utoptop  22251  restutop  22254  restutopopn  22255  ustuqtop1  22258  ustuqtop2  22259  ustuqtop3  22260  ustuqtop4  22261  utopreg  22269  ucncn  22302  fmucnd  22309  cfilufg  22310  trcfilu  22311  neipcfilu  22313  metustid  22572  metustsym  22573  metustexhalf  22574  metust  22576  cfilucfil  22577  metustbl  22584  psmetutop  22585  restmetu  22588  qdensere  22786  opnreen  22847  nmoleub2lem3  23127  ovolicc2lem4  23501  plydivlem4  24265  ulmuni  24360  dchrpt  25206  tgcgrtriv  25593  tgbtwntriv2  25596  tgbtwncom  25597  tgbtwnswapid  25601  tgbtwnintr  25602  tgbtwnouttr2  25604  tgtrisegint  25608  tgifscgr  25617  tgcgrxfr  25627  tgbtwnxfr  25639  motcgrg  25653  tgbtwnconn1lem3  25683  tgbtwnconn1  25684  tgbtwnconn3  25686  legval  25693  legov  25694  legov2  25695  legtrd  25698  legtri3  25699  legtrid  25700  ltgseg  25705  hlcgrex  25725  hlcgreulem  25726  colline  25758  miriso  25779  symquadlem  25798  krippenlem  25799  midexlem  25801  perpneq  25823  isperp2  25824  footex  25827  perpdrag  25834  colperpexlem3  25838  colperpex  25839  opphllem  25841  mideulem  25842  midex  25843  oppne3  25849  oppnid  25852  opphllem3  25855  opphllem5  25857  opphllem6  25858  oppperpex  25859  opphl  25860  outpasch  25861  hpgne1  25867  hpgne2  25868  lnopp2hpgb  25869  colopp  25875  lmieu  25890  lnperpex  25909  trgcopy  25910  trgcopyeulem  25911  acopy  25938  acopyeu  25939  inaghl  25945  cgrg3col4  25948  tgasa1  25953  f1otrg  25965  ttgbtwnid  25978  cnvbraval  29297  opsqrlem1  29327  rabfodom  29669  acunirnmpt  29786  acunirnmpt2  29787  acunirnmpt2f  29788  xrge0infss  29852  fsumiunle  29902  archirngz  30068  archiabllem1a  30070  archiabllem1b  30071  archiabllem1  30072  archiabllem2a  30073  archiabllem2c  30074  archiabl  30077  gsummpt2d  30106  fimaproj  30225  txomap  30226  qtophaus  30228  pcmplfinf  30253  pstmxmet  30265  pnfneige0  30322  esumcst  30450  esum2d  30480  esumiun  30481  ddemeas  30624  signsply0  30953  signstres  30977  prodfzo03  31006  actfunsnf1o  31007  actfunsnrndisj  31008  tgoldbachgt  31066  poimirlem17  33739  poimirlem20  33742  itg2gt0cn  33777  fdc1  33853  lhprelat3N  35820  dihjat2  37212  eldioph2b  37828  diophrex  37841  irrapxlem6  37893  pellex  37901  pellfundex  37952  lnrfg  38190  mpaaeu  38221  cvgdvgrat  39012  climsuse  40320  limsupre  40353  limcleqr  40356  xlimclim2lem  40545  climxlim2  40552  cncficcgt0  40581  dvbdfbdioo  40625  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  stoweidlem28  40724  stoweidlem29  40725  stoweidlem52  40748  stoweidlem60  40756  fourierdlem39  40842  fourierdlem102  40904  fourierdlem103  40905  fourierdlem104  40906  fourierdlem114  40916  hspmbllem2  41323  nnsum4primesevenALTV  42264