Theorem nfan 1900

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 1898	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ∧ 𝜓))
6	5	mptru 1544	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 398  ⊤wtru 1538  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnan  1901  nf3an  1902  hban  2308  nfeqf  2399  nfald2  2467  2ax6elem  2493  nfsb4t  2539  nfsb4tALT  2604  nfeu1ALT  2675  eupicka  2719  mopick2  2722  2mo  2733  clelab  2958  nfabd2  3002  nfabd2OLD  3003  2ralbida  3232  r19.12  3324  r19.29anOLD  3332  ralcom2  3363  reean  3366  cbvreuw  3443  cbvreu  3447  cbvrabw  3489  cbvrab  3490  ceqsex2  3543  vtocl2gaf  3576  spc2ed  3602  rspce  3612  eqvincf  3643  elrabf  3676  elrab3t  3679  rexab2  3691  rexab2OLD  3692  morex  3710  reu2  3716  rmo3f  3725  reu2eqd  3727  sbc2iegf  3849  reu8nf  3860  rmo2  3870  rmo3  3872  rmo3OLD  3873  csbiebt  3912  csbie2t  3921  cbvrabcsfw  3924  cbvreucsf  3927  cbvrabcsf  3928  reusngf  4612  rexreusng  4617  reuprg0  4638  rabsnifsb  4658  nfop  4819  nfopd  4820  eluniab  4853  iuneqconst  4930  nfopab  5134  cbvopab  5137  cbvopab1  5139  cbvopab1g  5140  cbvopab2  5141  cbvopab1s  5142  mpteq12f  5149  nfmpt  5163  cbvmptf  5165  cbvmptfg  5166  axrep3  5194  axrep4  5195  axrep5  5196  reusv2lem3  5301  axprlem4  5327  axprlem5  5328  nfpo  5479  nfso  5480  nffr  5529  nfwe  5531  nfxp  5588  opeliunxp  5619  nfco  5736  elrnmpt1  5830  nfimad  5938  reuop  6144  iota2  6344  nffun  6378  imadif  6438  nffn  6452  nff  6510  nff1  6573  nffo  6589  nff1o  6613  nffvd  6682  fv3  6688  fvmptdf  6774  f1ossf1o  6890  fmptco  6891  fsnex  7039  nfiso  7075  nfriotadw  7122  cbvriotaw  7123  nfriotad  7125  cbvriota  7127  riota2df  7137  riota5f  7142  oprabv  7214  nfoprab  7218  mpoeq123  7226  nfmpo  7236  cbvoprab1  7241  cbvoprab2  7242  cbvoprab12  7243  cbvoprab3  7245  cbvmpox  7247  ovmpodxf  7300  elovmporab  7391  elovmporab1w  7392  elovmporab1  7393  onminex  7522  peano5  7605  fiun  7644  f1iun  7645  opabex3d  7666  opabex3rd  7667  opabex3  7668  dfoprab4f  7754  fmpox  7765  opeliunxp2f  7876  nfwrecs  7949  wfrlem4  7958  tfr3  8035  tz7.49  8081  erovlem  8393  nfixpw  8480  nfixp  8481  nfixp1  8482  xpf1o  8679  nneneq  8700  ac6sfi  8762  nfoi  8978  wdom2d  9044  infpssrlem4  9728  hsmexlem2  9849  hsmexlem4  9851  domtriomlem  9864  axdc3lem2  9873  axdc4lem  9877  zorn2lem4  9921  zorn2lem5  9922  konigthlem  9990  axextnd  10013  axrepndlem2  10015  axrepnd  10016  axunnd  10018  axpowndlem2  10020  axpowndlem4  10022  axpownd  10023  axregndlem2  10025  axregnd  10026  axinfndlem1  10027  axinfnd  10028  zfcndrep  10036  zfcndinf  10040  dedekind  10803  dedekindle  10804  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  fsuppmapnn0fiubex  13361  reuccatpfxs1  14109  nfsum1  15046  nfsumw  15047  nfsum  15048  fsumsplitf  15098  fsum2dlem  15125  fsum00  15153  nfcprod1  15264  nfcprod  15265  fprod2dlem  15334  fprodsplitf  15342  fprodsplit1f  15344  fprodle  15350  lcmfunsnlem1  15981  lcmfunsnlem2lem1  15982  lcmfunsnlem2  15984  mreexexd  16919  acsmapd  17788  gsum2d2lem  19093  dprd2d2  19166  gsummoncoe1  20472  gsummatr01lem4  21267  cpmatmcllem  21326  cayleyhamilton1  21500  neiptopnei  21740  neiptopreu  21741  neitr  21788  iunconnlem  22035  iunconn  22036  ptcnplem  22229  ptcnp  22230  xkocnv  22422  isfildlem  22465  utopsnneiplem  22856  isucn2  22888  cfilucfil  23169  restmetu  23180  ovolfiniun  24102  ovoliunlem3  24105  ovoliunnul  24108  volfiniun  24148  itg2splitlem  24349  itg2split  24350  isibl2  24367  nfitg  24375  cbvitg  24376  limciun  24492  2sqmo  26013  2sqreulem4  26030  istrkg2ld  26246  chirred  30172  sbc2iedf  30230  rspc2daf  30231  opreu2reuALT  30240  mo5f  30253  foresf1o  30265  cbvdisjf  30321  disjabrex  30332  disjabrexf  30333  funimass4f  30382  fmptcof2  30402  fcomptf  30403  acunirnmpt2  30405  acunirnmpt2f  30406  aciunf1lem  30407  funcnv4mpt  30414  fnpreimac  30416  cnvoprabOLD  30456  f1od2  30457  fpwrelmap  30469  xrofsup  30492  nn0min  30536  fprodex01  30541  fsumiunle  30545  isarchiofld  30890  fedgmullem2  31026  reff  31103  locfinreflem  31104  cmpcref  31114  ordtconnlem1  31167  prodindf  31282  esumcl  31289  gsumesum  31318  esumlub  31319  esumcst  31322  esumrnmpt2  31327  esumfzf  31328  esumfsup  31329  hasheuni  31344  esumcvg  31345  esumgect  31349  esumcvgre  31350  esum2dlem  31351  esum2d  31352  esumiun  31353  ldsysgenld  31419  sigapildsyslem  31420  sigapildsys  31421  ldgenpisyslem1  31422  measvunilem  31471  measvunilem0  31472  measvuni  31473  measinblem  31479  voliune  31488  volfiniune  31489  volmeas  31490  oms0  31555  omssubadd  31558  eulerpartlemgvv  31634  dstrvprob  31729  breprexplema  31901  bnj919  32038  bnj1146  32063  bnj1379  32102  bnj849  32197  bnj916  32205  bnj964  32215  bnj1014  32233  bnj1123  32258  bnj1228  32283  bnj1307  32295  bnj1321  32299  bnj1398  32306  bnj1408  32308  bnj1444  32315  bnj1445  32316  bnj1446  32317  bnj1449  32320  bnj1467  32326  bnj1463  32327  bnj1489  32328  bnj1491  32329  bnj1312  32330  bnj1525  32341  cvmcov  32510  iota5f  32955  axextdist  33044  axextbdist  33045  trpredmintr  33070  nfwlim  33109  nffrecs  33120  frrlem4  33126  finminlem  33666  bj-dvelimdv  34175  isbasisrelowllem1  34639  isbasisrelowllem2  34640  fvineqsneu  34695  fvineqsneq  34696  wl-cbvalnaed  34787  wl-2sb6d  34809  wl-sbalnae  34813  wl-mo2tf  34822  wl-eutf  34824  wl-ax11-lem3  34834  phpreu  34891  poimirlem26  34933  poimirlem27  34934  heicant  34942  mbfposadd  34954  ftc1anclem5  34986  indexdom  35024  filbcmb  35030  sdclem2  35032  sdclem1  35033  fdc1  35036  riotasv2d  36108  riotasv2s  36109  nfded2  36119  glbconxN  36529  pmapglb2xN  36923  cdlemefs32sn1aw  37565  mzpsubmpt  39389  mzpexpmpt  39391  eq0rabdioph  39422  eqrabdioph  39423  setindtr  39670  ss2iundf  40053  scottabf  40625  mnuprdlem4  40660  binomcxplemnotnn0  40737  iunconnlem2  41318  elunif  41322  rspcegf  41329  fnchoice  41335  refsumcn  41336  rfcnnnub  41342  uzwo4  41364  fiiuncl  41376  cbvmpo2  41412  cbvmpo1  41413  iinssiin  41444  ralimda  41455  disjf1  41492  disjrnmpt2  41498  disjf1o  41501  fompt  41502  disjinfi  41503  choicefi  41512  axccdom  41536  dmrelrnrel  41539  axccd  41544  funimassd  41546  rnmptbddlem  41564  rnmptbd2lem  41569  infnsuprnmpt  41571  rnmptbdlem  41576  rnmptssbi  41583  upbdrech  41621  ssfiunibd  41625  supxrgere  41650  supxrgelem  41654  supxrge  41655  xralrple2  41671  infxr  41684  infxrunb2  41685  xrralrecnnle  41702  xrralrecnnge  41711  supxrunb3  41721  supxrleubrnmpt  41728  infleinf2  41737  unb2ltle  41738  rexabslelem  41741  suprleubrnmpt  41745  uzub  41754  supminfrnmpt  41768  supxrleubrnmptf  41776  infxrgelbrnmpt  41779  infrpgernmpt  41790  monoordxr  41808  monoord2xr  41810  iccshift  41843  iooshift  41847  iooiinicc  41867  iooiinioc  41881  fsumclf  41899  fsummulc1f  41900  fsumsplit1  41902  fsumf1of  41904  fsumreclf  41906  fsumlessf  41907  fmul01  41910  fmuldfeqlem1  41912  fmuldfeq  41913  fmul01lt1lem1  41914  fmul01lt1lem2  41915  fprodexp  41924  mccl  41928  fprodcnlem  41929  fprodcn  41930  climmulf  41934  climexp  41935  climsuse  41938  climrecf  41939  climinff  41941  climaddf  41945  mullimc  41946  islptre  41949  climf  41952  mullimcf  41953  rexlim2d  41955  idlimc  41956  limcperiod  41958  limcrecl  41959  islpcn  41969  limsupre  41971  limcleqr  41974  addlimc  41978  limclner  41981  climsubmpt  41990  climreclf  41994  climf2  41996  climeldmeqmpt  41998  clim2f2  42000  climfveqmpt  42001  fnlimfvre  42004  allbutfifvre  42005  climleltrp  42006  fnlimf  42008  fnlimabslt  42009  climfveqf  42010  climfveqmpt3  42012  climeldmeqf  42013  climeqf  42018  climeldmeqmpt3  42019  limsuppnfd  42032  limsupub  42034  climinf2lem  42036  climinf2  42037  limsuppnf  42041  limsupubuz  42043  climinf2mpt  42044  climinfmpt  42045  climinf3  42046  limsupmnflem  42050  limsupequz  42053  limsupre2  42055  limsupmnfuzlem  42056  limsupequzmptf  42061  limsupre3  42063  limsupre3uzlem  42065  limsupreuzmpt  42069  climisp  42076  lmbr3  42077  climrescn  42078  climxrrelem  42079  climxrre  42080  limsupub2  42142  liminflbuz2  42145  xlimmnfvlem2  42163  xlimmnfv  42164  xlimpnfvlem2  42167  xlimpnfv  42168  xlimmnfmpt  42173  xlimpnfmpt  42174  climxlim2lem  42175  cncficcgt0  42220  cncfioobd  42229  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  dvmptmulf  42271  dvnmul  42277  dvmptfprodlem  42278  dvmptfprod  42279  dvnprodlem1  42280  dvnprodlem2  42281  iblsplitf  42304  itgperiod  42315  stoweidlem3  42337  stoweidlem26  42360  stoweidlem27  42361  stoweidlem29  42363  stoweidlem31  42365  stoweidlem34  42368  stoweidlem35  42369  stoweidlem36  42370  stoweidlem39  42373  stoweidlem42  42376  stoweidlem43  42377  stoweidlem44  42378  stoweidlem46  42380  stoweidlem48  42382  stoweidlem49  42383  stoweidlem51  42385  stoweidlem52  42386  stoweidlem53  42387  stoweidlem54  42388  stoweidlem55  42389  stoweidlem56  42390  stoweidlem57  42391  stoweidlem58  42392  stoweidlem59  42393  stoweidlem60  42394  stoweidlem61  42395  stoweidlem62  42396  stoweid  42397  wallispilem3  42401  stirlinglem13  42420  stirling  42423  fourierdlem16  42457  fourierdlem21  42462  fourierdlem22  42463  fourierdlem31  42472  fourierdlem39  42480  fourierdlem48  42488  fourierdlem51  42491  fourierdlem53  42493  fourierdlem68  42508  fourierdlem71  42511  fourierdlem73  42513  fourierdlem80  42520  fourierdlem81  42521  fourierdlem86  42526  fourierdlem87  42527  fourierdlem93  42533  fourierdlem94  42534  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  fourierdlem113  42553  elaa2  42568  etransclem32  42600  salexct  42666  sge0revalmpt  42709  sge0f1o  42713  sge0lefi  42729  sge0resplit  42737  sge0lempt  42741  sge0iunmptlemre  42746  sge0fodjrnlem  42747  sge0iunmpt  42749  sge0ltfirpmpt2  42757  sge0isum  42758  sge0xp  42760  sge0isummpt2  42763  sge0xadd  42766  sge0pnffsumgt  42773  sge0gtfsumgt  42774  sge0uzfsumgt  42775  sge0reuz  42778  sge0reuzb  42779  iundjiun  42791  meadjiun  42797  ismeannd  42798  voliunsge0lem  42803  meaiunincf  42814  meaiuninc3v  42815  meaiuninc3  42816  meaiininc  42818  caragenfiiuncl  42846  omeiunltfirp  42850  ovnsubaddlem2  42902  hoidmvval0  42918  hoidmvlelem1  42926  hoidmvlelem3  42928  hoidmvlelem5  42930  ovnlecvr2  42941  hspdifhsp  42947  hoiqssbllem2  42954  hoiqssbllem3  42955  hspmbllem2  42958  opnvonmbllem2  42964  hoimbl2  42996  vonhoire  43003  iinhoiicc  43005  iunhoiioolem  43006  iunhoiioo  43007  vonioo  43013  vonicc  43016  vonn0ioo2  43021  vonn0icc2  43023  salpreimagelt  43035  salpreimalegt  43037  pimincfltioc  43043  pimdecfgtioo  43044  pimincfltioo  43045  preimageiingt  43047  preimaleiinlt  43048  salpreimagtge  43051  salpreimaltle  43052  salpreimalelt  43055  salpreimagtlt  43056  incsmflem  43067  issmflelem  43070  issmfle  43071  smfconst  43075  issmfgtlem  43081  issmfgt  43082  smfaddlem2  43089  smfadd  43090  decsmflem  43091  decsmf  43092  issmfgelem  43094  issmfge  43095  smflimlem2  43097  smflim  43102  smfresal  43112  smfrec  43113  smfmullem4  43118  smfmul  43119  smfpimcc  43131  smflimmpt  43133  smfsuplem1  43134  smfsupmpt  43138  smfsupxr  43139  smfinflem  43140  smfinfmpt  43142  smflimsuplem5  43147  smflimsuplem7  43149  smflimsuplem8  43150  smflimsupmpt  43152  smfliminflem  43153  smfliminfmpt  43155  or2expropbilem2  43317  or2expropbi  43318  2reu8i  43361  nfdfat  43375  iccelpart  43642  ichnfim  43673  ich2exprop  43682  ichreuopeq  43684  sprsymrelfo  43708  reupr  43733  reuopreuprim  43737  2zrngmmgm  44266  opeliun2xp  44430  cbvmpox2  44433  ovmpordxf  44436  setrec1  44843  aacllem  44951