Theorem nfan 1862

Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ∧ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 9-Oct-2021.)

Hypotheses

Ref	Expression
nfan.1	⊢ Ⅎ𝑥𝜑
nfan.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfan	⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Proof of Theorem nfan

Step	Hyp	Ref	Expression
1		nfan.1	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
3		nfan.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜓)
5	2, 4	nfand 1860	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ∧ 𝜓))
6	5	mptru 1514	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 387  ⊤wtru 1508  Ⅎwnf 1746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747

This theorem is referenced by:  nfnan  1863  nf3an  1864  hban  2234  nfeqf  2311  nfald2  2381  2ax6elem  2416  nfsb4t  2460  nfsb4tALT  2531  nfeu1ALT  2608  eupicka  2665  mopick2  2668  2mo  2679  axbndOLD  2749  clelab  2913  nfabd2  2953  nfabd2OLD  2954  2ralbida  3179  r19.12  3265  r19.29anOLD  3273  ralcom2  3304  reean  3307  cbvreu  3381  cbvrab  3411  ceqsex2  3464  vtocl2gaf  3495  spc2ed  3520  rspce  3530  eqvincf  3558  elrabf  3591  elrab3t  3594  rexab2  3606  morex  3626  reu2  3630  rmo3f  3639  reu2eqd  3641  sbc2iegf  3754  reu8nf  3765  rmo2  3775  rmo3  3777  rmo3OLD  3778  csbiebt  3810  csbie2t  3819  cbvreucsf  3824  cbvrabcsf  3825  reusngf  4487  rexreusng  4492  reuprg0  4513  rabsnifsb  4533  nfop  4694  nfopd  4695  eluniab  4724  nfopab  4998  cbvopab  5001  cbvopab1  5003  cbvopab2  5004  cbvopab1s  5005  mpteq12f  5011  nfmpt  5025  cbvmptf  5027  cbvmpt  5028  axrep3  5054  axrep4  5055  axrep5  5056  reusv2lem3  5155  axprlem4  5184  axprlem5  5185  nfpo  5332  nfso  5333  nffr  5382  nfwe  5384  nfxp  5441  opeliunxp  5470  nfco  5587  elrnmpt1  5674  nfimad  5781  reuop  5984  iota2  6180  nffun  6213  imadif  6273  nffn  6287  nff  6342  nff1  6404  nffo  6420  nff1o  6444  nffvd  6513  fv3  6519  f1ossf1o  6715  fmptco  6716  fsnex  6866  nfiso  6900  nfriotad  6947  cbvriota  6949  riota2df  6959  riota5f  6964  oprabv  7035  nfoprab  7039  mpoeq123  7046  nfmpo  7056  cbvoprab1  7059  cbvoprab2  7060  cbvoprab12  7061  cbvoprab3  7063  cbvmpox  7065  ovmpodxf  7118  elovmporab  7212  elovmporab1  7213  onminex  7340  peano5  7422  fun11iun  7460  opabex3d  7480  opabex3rd  7481  opabex3  7482  dfoprab4f  7564  fmpox  7575  opeliunxp2f  7681  nfwrecs  7754  wfrlem4  7763  wfrlem4OLD  7764  tfr3  7841  tz7.49  7886  erovlem  8195  nfixp  8280  nfixp1  8281  xpf1o  8477  nneneq  8498  ac6sfi  8559  nfoi  8775  wdom2d  8841  infpssrlem4  9528  hsmexlem2  9649  hsmexlem4  9651  domtriomlem  9664  axdc3lem2  9673  axdc4lem  9677  zorn2lem4  9721  zorn2lem5  9722  konigthlem  9790  axextnd  9813  axrepndlem2  9815  axrepnd  9816  axunnd  9818  axpowndlem2  9820  axpowndlem4  9822  axpownd  9823  axregndlem2  9825  axregnd  9826  axinfndlem1  9827  axinfnd  9828  zfcndrep  9836  zfcndinf  9840  dedekind  10605  dedekindle  10606  fsuppmapnn0fiublem  13176  fsuppmapnn0fiub  13177  fsuppmapnn0fiubex  13178  reuccats1OLD  13924  reuccatpfxs1  13959  nfsum1  14910  nfsum  14911  fsumsplitf  14961  fsum2dlem  14988  fsum00  15016  nfcprod1  15127  nfcprod  15128  fprod2dlem  15197  fprodsplitf  15205  fprodsplit1f  15207  fprodle  15213  lcmfunsnlem1  15840  lcmfunsnlem2lem1  15841  lcmfunsnlem2  15843  mreexexd  16780  acsmapd  17649  gsum2d2lem  18849  dprd2d2  18919  gsummoncoe1  20178  gsummatr01lem4  20974  cpmatmcllem  21033  cayleyhamilton1  21207  neiptopnei  21447  neiptopreu  21448  neitr  21495  iunconnlem  21742  iunconn  21743  ptcnplem  21936  ptcnp  21937  xkocnv  22129  isfildlem  22172  utopsnneiplem  22562  isucn2  22594  cfilucfil  22875  restmetu  22886  ovolfiniun  23808  ovoliunlem3  23811  ovoliunnul  23814  volfiniun  23854  itg2splitlem  24055  itg2split  24056  isibl2  24073  nfitg  24081  cbvitg  24082  limciun  24198  2sqmo  25718  2sqreulem4  25735  istrkg2ld  25951  chirred  29956  sbc2iedf  30014  rspc2daf  30015  opreu2reuALT  30025  mo5f  30038  foresf1o  30047  cbvdisjf  30091  disjabrex  30101  disjabrexf  30102  funimass4f  30147  fmptcof2  30167  fcomptf  30168  acunirnmpt2  30170  acunirnmpt2f  30171  aciunf1lem  30172  funcnv4mpt  30179  fnpreimac  30181  cnvoprabOLD  30211  f1od2  30212  fpwrelmap  30224  xrofsup  30247  nn0min  30286  fprodex01  30290  fsumiunle  30294  isarchiofld  30569  fedgmullem2  30655  reff  30747  locfinreflem  30748  cmpcref  30758  ordtconnlem1  30811  prodindf  30926  esumcl  30933  gsumesum  30962  esumlub  30963  esumcst  30966  esumrnmpt2  30971  esumfzf  30972  esumfsup  30973  hasheuni  30988  esumcvg  30989  esumgect  30993  esumcvgre  30994  esum2dlem  30995  esum2d  30996  esumiun  30997  ldsysgenld  31064  sigapildsyslem  31065  sigapildsys  31066  ldgenpisyslem1  31067  measvunilem  31116  measvunilem0  31117  measvuni  31118  measinblem  31124  voliune  31133  volfiniune  31134  volmeas  31135  oms0  31200  omssubadd  31203  eulerpartlemgvv  31279  dstrvprob  31375  breprexplema  31549  bnj919  31686  bnj1146  31711  bnj1379  31750  bnj849  31844  bnj916  31852  bnj964  31862  bnj1014  31879  bnj1123  31903  bnj1228  31928  bnj1307  31940  bnj1321  31944  bnj1398  31951  bnj1408  31953  bnj1444  31960  bnj1445  31961  bnj1446  31962  bnj1449  31965  bnj1467  31971  bnj1463  31972  bnj1489  31973  bnj1491  31974  bnj1312  31975  bnj1525  31986  cvmcov  32095  iota5f  32475  axextdist  32565  axext4dist  32566  trpredmintr  32591  nfwlim  32630  nffrecs  32641  frrlem4  32647  finminlem  33187  bj-axrep3  33620  bj-axrep4  33621  bj-axrep5  33622  bj-dvelimdv  33666  isbasisrelowllem1  34078  isbasisrelowllem2  34079  fvineqsneu  34133  fvineqsneq  34134  wl-cbvalnaed  34214  wl-2sb6d  34235  wl-sbalnae  34239  wl-mo2tf  34248  wl-eutf  34250  wl-ax11-lem3  34260  phpreu  34317  poimirlem26  34359  poimirlem27  34360  heicant  34368  mbfposadd  34380  ftc1anclem5  34412  indexdom  34451  filbcmb  34457  sdclem2  34459  sdclem1  34460  fdc1  34463  riotasv2d  35538  riotasv2s  35539  nfded2  35549  glbconxN  35959  pmapglb2xN  36353  cdlemefs32sn1aw  36995  mzpsubmpt  38735  mzpexpmpt  38737  eq0rabdioph  38769  eqrabdioph  38770  setindtr  39017  ss2iundf  39367  scottabf  39951  mnuprdlem4  39986  binomcxplemnotnn0  40104  iunconnlem2  40688  elunif  40692  rspcegf  40699  fnchoice  40705  refsumcn  40706  rfcnnnub  40712  uzwo4  40735  fiiuncl  40747  cbvmpt22  40786  cbvmpt21  40787  iinssiin  40818  ralimda  40829  disjf1  40868  disjrnmpt2  40874  disjf1o  40877  fompt  40878  disjinfi  40879  choicefi  40889  axccdom  40913  dmrelrnrel  40916  axccd  40922  funimassd  40924  rnmptbddlem  40943  rnmptbd2lem  40949  infnsuprnmpt  40951  rnmptbdlem  40956  rnmptssbi  40963  upbdrech  41002  ssfiunibd  41006  supxrgere  41031  supxrgelem  41035  supxrge  41036  xralrple2  41052  infxr  41065  infxrunb2  41066  xrralrecnnle  41084  xrralrecnnge  41093  supxrunb3  41103  supxrleubrnmpt  41111  infleinf2  41120  unb2ltle  41121  rexabslelem  41124  suprleubrnmpt  41128  uzub  41137  supminfrnmpt  41151  supxrleubrnmptf  41159  infxrgelbrnmpt  41162  infrpgernmpt  41173  monoordxr  41191  monoord2xr  41193  iccshift  41226  iooshift  41230  iooiinicc  41250  iooiinioc  41264  fsumclf  41282  fsummulc1f  41283  fsumsplit1  41285  fsumf1of  41287  fsumreclf  41289  fsumlessf  41290  fmul01  41293  fmuldfeqlem1  41295  fmuldfeq  41296  fmul01lt1lem1  41297  fmul01lt1lem2  41298  fprodexp  41307  mccl  41311  fprodcnlem  41312  fprodcn  41313  climmulf  41317  climexp  41318  climsuse  41321  climrecf  41322  climinff  41324  climaddf  41328  mullimc  41329  islptre  41332  climf  41335  mullimcf  41336  rexlim2d  41338  idlimc  41339  limcperiod  41341  limcrecl  41342  islpcn  41352  limsupre  41354  limcleqr  41357  addlimc  41361  limclner  41364  climsubmpt  41373  climreclf  41377  climf2  41379  climeldmeqmpt  41381  clim2f2  41383  climfveqmpt  41384  fnlimfvre  41387  allbutfifvre  41388  climleltrp  41389  fnlimf  41391  fnlimabslt  41392  climfveqf  41393  climfveqmpt3  41395  climeldmeqf  41396  climeqf  41401  climeldmeqmpt3  41402  limsuppnfd  41415  limsupub  41417  climinf2lem  41419  climinf2  41420  limsuppnf  41424  limsupubuz  41426  climinf2mpt  41427  climinfmpt  41428  climinf3  41429  limsupmnflem  41433  limsupequz  41436  limsupre2  41438  limsupmnfuzlem  41439  limsupequzmptf  41444  limsupre3  41446  limsupre3uzlem  41448  limsupreuzmpt  41452  climisp  41459  lmbr3  41460  climrescn  41461  climxrrelem  41462  climxrre  41463  limsupub2  41525  liminflbuz2  41528  xlimmnfvlem2  41546  xlimmnfv  41547  xlimpnfvlem2  41550  xlimpnfv  41551  xlimmnfmpt  41556  xlimpnfmpt  41557  climxlim2lem  41558  cncficcgt0  41602  cncfioobd  41611  fprodsubrecnncnvlem  41622  fprodaddrecnncnvlem  41624  dvmptmulf  41653  dvnmul  41659  dvmptfprodlem  41660  dvmptfprod  41661  dvnprodlem1  41662  dvnprodlem2  41663  iblsplitf  41686  itgperiod  41697  stoweidlem3  41720  stoweidlem26  41743  stoweidlem27  41744  stoweidlem29  41746  stoweidlem31  41748  stoweidlem34  41751  stoweidlem35  41752  stoweidlem36  41753  stoweidlem39  41756  stoweidlem42  41759  stoweidlem43  41760  stoweidlem44  41761  stoweidlem46  41763  stoweidlem48  41765  stoweidlem49  41766  stoweidlem51  41768  stoweidlem52  41769  stoweidlem53  41770  stoweidlem54  41771  stoweidlem55  41772  stoweidlem56  41773  stoweidlem57  41774  stoweidlem58  41775  stoweidlem59  41776  stoweidlem60  41777  stoweidlem61  41778  stoweidlem62  41779  stoweid  41780  wallispilem3  41784  stirlinglem13  41803  stirling  41806  fourierdlem16  41840  fourierdlem21  41845  fourierdlem22  41846  fourierdlem31  41855  fourierdlem39  41863  fourierdlem48  41871  fourierdlem51  41874  fourierdlem53  41876  fourierdlem68  41891  fourierdlem71  41894  fourierdlem73  41896  fourierdlem80  41903  fourierdlem81  41904  fourierdlem86  41909  fourierdlem87  41910  fourierdlem93  41916  fourierdlem94  41917  fourierdlem103  41926  fourierdlem104  41927  fourierdlem112  41935  fourierdlem113  41936  elaa2  41951  etransclem32  41983  salexct  42049  sge0revalmpt  42092  sge0f1o  42096  sge0lefi  42112  sge0resplit  42120  sge0lempt  42124  sge0iunmptlemre  42129  sge0fodjrnlem  42130  sge0iunmpt  42132  sge0ltfirpmpt2  42140  sge0isum  42141  sge0xp  42143  sge0isummpt2  42146  sge0xadd  42149  sge0pnffsumgt  42156  sge0gtfsumgt  42157  sge0uzfsumgt  42158  sge0reuz  42161  sge0reuzb  42162  iundjiun  42174  meadjiun  42180  ismeannd  42181  voliunsge0lem  42186  meaiunincf  42197  meaiuninc3v  42198  meaiuninc3  42199  meaiininc  42201  caragenfiiuncl  42229  omeiunltfirp  42233  ovnsubaddlem2  42285  hoidmvval0  42301  hoidmvlelem1  42309  hoidmvlelem3  42311  hoidmvlelem5  42313  ovnlecvr2  42324  hspdifhsp  42330  hoiqssbllem2  42337  hoiqssbllem3  42338  hspmbllem2  42341  opnvonmbllem2  42347  hoimbl2  42379  vonhoire  42386  iinhoiicc  42388  iunhoiioolem  42389  iunhoiioo  42390  vonioo  42396  vonicc  42399  vonn0ioo2  42404  vonn0icc2  42406  salpreimagelt  42418  salpreimalegt  42420  pimincfltioc  42426  pimdecfgtioo  42427  pimincfltioo  42428  preimageiingt  42430  preimaleiinlt  42431  salpreimagtge  42434  salpreimaltle  42435  salpreimalelt  42438  salpreimagtlt  42439  incsmflem  42450  issmflelem  42453  issmfle  42454  smfconst  42458  issmfgtlem  42464  issmfgt  42465  smfaddlem2  42472  smfadd  42473  decsmflem  42474  decsmf  42475  issmfgelem  42477  issmfge  42478  smflimlem2  42480  smflim  42485  smfresal  42495  smfrec  42496  smfmullem4  42501  smfmul  42502  smfpimcc  42514  smflimmpt  42516  smfsuplem1  42517  smfsupmpt  42521  smfsupxr  42522  smfinflem  42523  smfinfmpt  42525  smflimsuplem5  42530  smflimsuplem7  42532  smflimsuplem8  42533  smflimsupmpt  42535  smfliminflem  42536  smfliminfmpt  42538  or2expropbilem2  42674  or2expropbi  42675  2reu8i  42719  nfdfat  42733  iccelpart  42966  ichnfim  42995  ich2exprop  43002  ichreuopeq  43004  sprsymrelfo  43028  reupr  43053  reuopreuprim  43057  2zrngmmgm  43582  opeliun2xp  43746  cbvmpt2x2  43749  ovmpt2rdxf  43752  setrec1  44162  aacllem  44270