Theorem nfan 1913

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

Syntax hints:   ∧ wa 398  ⊤wtru 1555  Ⅎwnf 1797

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1557  df-ex 1794  df-nf 1798

This theorem is referenced by:  nfnan  1914  nf3an  1915  hban  2328  nfeqf  2406  nfald2  2470  2ax6elem  2495  nfsb4t  2524  nfeu1  2610  eupicka  2655  mopick2  2658  2mo  2669  nfabd2  2941  2ralbida  3279  r19.12  3305  reean  3306  ralcom2  3358  cbvrmow  3386  nfrmow  3390  nfreuw  3391  cbvreu  3400  cbvrabw  3443  cbvrabwOLD  3444  nfrabw  3445  cbvrab  3447  ceqsex2  3498  vtocl3gaf  3539  spc2ed  3555  rspce  3565  eqvincf  3604  elrabf  3642  elrab3t  3644  rexab2  3656  morex  3676  reu2  3682  rmo3f  3691  reu2eqd  3693  sbc2iegf  3813  reu8nf  3825  rmo2  3835  rmo3  3837  csbiebt  3876  csbie2t  3885  cbvrabcsfw  3888  cbvreucsf  3891  cbvrabcsf  3892  nfdif  4078  nfin  4171  reusngf  4627  rexreusng  4632  reuprg0  4655  rabsnifsb  4675  nfop  4841  nfopd  4842  eluniab  4873  iuneqconst  4955  cbvopab  5166  cbvopab1  5168  cbvopab1g  5169  cbvopab2  5170  cbvopab1s  5171  mpteq12f  5179  nfmpt  5192  cbvmptf  5194  cbvmptfg  5195  axrep3  5225  axrep4OLD  5228  axrep5  5229  reusv2lem3  5351  axprlem4OLD  5381  axprlem5OLD  5382  nfpo  5554  nfso  5555  nffr  5613  nfwe  5615  nfxp  5673  opeliunxp  5707  opeliun2xp  5708  nfco  5830  elrnmpt1  5929  nfimad  6048  reuop  6269  iota2  6499  nffun  6533  imadif  6594  nffn  6609  nff  6676  nff1  6747  nffo  6766  nff1o  6793  nffvd  6868  fv3  6874  funimassd  6922  fvmptdf  6971  fompt  7088  f1ossf1o  7099  fmptco  7100  fsnex  7256  nfiso  7295  nfriotadw  7350  cbvriotaw  7351  nfriotad  7353  cbvriota  7355  riota2df  7365  riota5f  7370  oprabv  7445  nfoprab  7449  mpoeq123  7457  nfmpo  7467  cbvoprab1  7472  cbvoprab2  7473  cbvoprab12  7474  cbvoprab3  7476  cbvmpox  7478  ovmpodxf  7535  elovmporab  7631  elovmporab1w  7632  elovmporab1  7633  onminex  7774  fiun  7913  f1iun  7914  opabex3d  7935  opabex3rd  7936  opabex3  7937  dfoprab4f  8026  fmpox  8037  opeliunxp2f  8178  nffrecs  8252  frrlem4  8258  tfr3  8358  tz7.49  8404  naddsuc2  8660  erovlem  8783  nfixpw  8887  nfixp  8888  nfixp1  8889  xpf1o  9100  nneneq  9163  ac6sfi  9217  nfoi  9452  wdom2d  9518  infpssrlem4  10253  hsmexlem2  10374  hsmexlem4  10376  domtriomlem  10389  axdc3lem2  10398  axdc4lem  10402  zorn2lem4  10446  zorn2lem5  10447  konigthlem  10516  axextnd  10539  axrepndlem2  10541  axrepnd  10542  axunnd  10544  axpowndlem2  10546  axpowndlem4  10548  axpownd  10549  axregndlem2  10551  axregnd  10552  axinfndlem1  10553  axinfnd  10554  zfcndrep  10562  zfcndinf  10566  dedekind  11336  dedekindle  11337  fsuppmapnn0fiublem  13993  fsuppmapnn0fiub  13994  fsuppmapnn0fiubex  13995  reuccatpfxs1  14750  nfsum1  15693  nfsum  15694  fsumclf  15741  fsumsplitf  15745  fsumsplit1  15748  fsum2dlem  15773  fsum00  15802  nfcprod1  15914  nfcprod  15915  fprod2dlem  15986  fprodsplitf  15994  fprodsplit1f  15996  fprodle  16002  lcmfunsnlem1  16647  lcmfunsnlem2lem1  16648  lcmfunsnlem2  16650  mreexexd  17656  acsmapd  18562  gsum2d2lem  19989  dprd2d2  20062  gsummoncoe1  22344  gsummatr01lem4  22691  cpmatmcllem  22751  cayleyhamilton1  22925  neiptopnei  23165  neiptopreu  23166  neitr  23213  iunconnlem  23460  iunconn  23461  ptcnplem  23654  ptcnp  23655  xkocnv  23847  isfildlem  23890  utopsnneiplem  24280  isucn2  24311  cfilucfil  24592  restmetu  24603  ovolfiniun  25536  ovoliunlem3  25539  ovoliunnul  25542  volfiniun  25582  itg2splitlem  25783  itg2split  25784  isibl2  25801  nfitg  25810  cbvitg  25811  limciun  25929  2sqmo  27471  2sqreulem4  27488  bdaypw2n0bndlem  28526  istrkg2ld  28599  chirred  32537  sbc2iedf  32605  rspc2daf  32606  opreu2reuALT  32617  mo5f  32629  foresf1o  32645  iinabrex  32711  cbvdisjf  32713  disjabrex  32724  disjabrexf  32725  funimass4f  32782  2ndresdju  32794  fmptcof2  32802  fcomptf  32803  acunirnmpt2  32805  acunirnmpt2f  32806  aciunf1lem  32807  funcnv4mpt  32813  fnpreimac  32815  f1od2  32864  fpwrelmap  32878  xrofsup  32912  nn0min  32966  fprodex01  32970  fsumiunle  32974  prodindf  32994  suppgsumssiun  33206  isarchiofld  33333  elrgspnsubrunlem2  33383  nsgqusf1olem1  33553  nsgqusf1olem3  33555  elrspunidl  33568  deg1prod  33733  mplvrpmga  33796  esplyfval1  33824  vieta  33831  fedgmullem2  33881  irngnzply1  33942  reff  34090  locfinreflem  34091  cmpcref  34101  zarclsiin  34122  zarcmplem  34132  ordtconnlem1  34175  esumcl  34281  gsumesum  34310  esumlub  34311  esumcst  34314  esumrnmpt2  34319  esumfzf  34320  esumfsup  34321  hasheuni  34336  esumcvg  34337  esumgect  34341  esumcvgre  34342  esum2dlem  34343  esum2d  34344  esumiun  34345  ldsysgenld  34411  sigapildsyslem  34412  sigapildsys  34413  ldgenpisyslem1  34414  measvunilem  34463  measvunilem0  34464  measvuni  34465  measinblem  34471  voliune  34480  volfiniune  34481  volmeas  34482  oms0  34548  omssubadd  34551  eulerpartlemgvv  34627  dstrvprob  34723  breprexplema  34881  bnj919  35020  bnj1146  35043  bnj1379  35082  bnj849  35177  bnj916  35185  bnj964  35195  bnj1014  35213  bnj1123  35238  bnj1228  35263  bnj1307  35275  bnj1321  35279  bnj1398  35286  bnj1408  35288  bnj1444  35295  bnj1445  35296  bnj1446  35297  bnj1449  35300  bnj1467  35306  bnj1463  35307  bnj1489  35308  bnj1491  35309  bnj1312  35310  bnj1525  35321  dvelimalcased  35327  dvelimexcased  35329  fineqvrep  35365  cvmcov  35561  iota5f  36022  axextdist  36095  axextbdist  36096  nfwlim  36118  finminlem  36626  axtcond  36786  bj-dvelimdv  37284  bj-axreprepsep  37508  bj-opabco  37628  isbasisrelowllem1  37797  isbasisrelowllem2  37798  fvineqsneu  37853  fvineqsneq  37854  wl-cbvalnaed  37983  wl-2sb6d  38009  wl-sbalnae  38013  wl-mo2tf  38022  wl-eutf  38024  phpreu  38051  poimirlem26  38093  poimirlem27  38094  heicant  38102  mbfposadd  38114  ftc1anclem5  38144  indexdom  38181  filbcmb  38187  sdclem2  38189  sdclem1  38190  fdc1  38193  riotasv2d  39529  riotasv2s  39530  nfded2  39540  glbconxN  39950  pmapglb2xN  40344  cdlemefs32sn1aw  40986  mzpsubmpt  43272  mzpexpmpt  43274  eq0rabdioph  43305  eqrabdioph  43306  setindtr  43549  unielss  43743  nadd1suc  43917  ss2iundf  44183  scottabf  44764  mnuprdlem4  44799  ismnushort  44825  binomcxplemnotnn0  44880  iunconnlem2  45458  nfrelp  45473  modelaxreplem3  45504  modelaxrep  45505  permaxrep  45530  elunif  45544  rspcegf  45551  fnchoice  45557  refsumcn  45558  rfcnnnub  45564  uzwo4  45581  fiiuncl  45593  cbvmpo2  45623  cbvmpo1  45624  iinssiin  45655  disjf1  45709  disjrnmpt2  45714  disjf1o  45717  disjinfi  45718  choicefi  45725  axccdom  45746  dmrelrnrel  45750  axccd  45752  rnmptbddlem  45767  rnmptbd2lem  45771  infnsuprnmpt  45773  rnmptbdlem  45778  rnmptssbi  45783  upbdrech  45832  ssfiunibd  45836  supxrgere  45857  supxrgelem  45861  supxrge  45862  xralrple2  45878  infxr  45890  infxrunb2  45891  xrralrecnnle  45906  xrralrecnnge  45913  supxrunb3  45922  supxrleubrnmpt  45928  infleinf2  45936  unb2ltle  45937  rexabslelem  45940  suprleubrnmpt  45944  uzub  45953  supminfrnmpt  45967  supxrleubrnmptf  45973  infxrgelbrnmpt  45976  infrpgernmpt  45987  monoordxr  46004  monoord2xr  46006  caucvgbf  46011  cvgcaule  46013  iccshift  46042  iooshift  46046  iooiinicc  46066  iooiinioc  46080  fsummulc1f  46095  fsumf1of  46098  fsumreclf  46100  fsumlessf  46101  fmul01  46104  fmuldfeqlem1  46106  fmuldfeq  46107  fmul01lt1lem1  46108  fmul01lt1lem2  46109  fprodexp  46118  mccl  46122  fprodcnlem  46123  fprodcn  46124  climmulf  46128  climexp  46129  climsuse  46132  climrecf  46133  climinff  46135  climaddf  46139  mullimc  46140  islptre  46143  climf  46146  mullimcf  46147  rexlim2d  46149  idlimc  46150  limcperiod  46152  limcrecl  46153  islpcn  46161  limsupre  46163  limcleqr  46166  addlimc  46170  limclner  46173  climsubmpt  46182  climreclf  46186  climf2  46188  climeldmeqmpt  46190  clim2f2  46192  climfveqmpt  46193  fnlimfvre  46196  allbutfifvre  46197  climleltrp  46198  fnlimf  46200  fnlimabslt  46201  climfveqf  46202  climfveqmpt3  46204  climeldmeqf  46205  climeqf  46210  climeldmeqmpt3  46211  limsuppnfd  46224  limsupub  46226  climinf2lem  46228  climinf2  46229  limsuppnf  46233  limsupubuz  46235  climinf2mpt  46236  climinfmpt  46237  climinf3  46238  limsupmnflem  46242  limsupequz  46245  limsupre2  46247  limsupmnfuzlem  46248  limsupequzmptf  46253  limsupre3  46255  limsupre3uzlem  46257  limsupreuzmpt  46261  climisp  46268  lmbr3  46269  climrescn  46270  climxrrelem  46271  climxrre  46272  limsupub2  46334  liminflbuz2  46337  xlimmnfvlem2  46355  xlimmnfv  46356  xlimpnfvlem2  46359  xlimpnfv  46360  xlimmnfmpt  46365  xlimpnfmpt  46366  climxlim2lem  46367  cncficcgt0  46410  cncfioobd  46419  fprodsubrecnncnvlem  46429  fprodaddrecnncnvlem  46431  dvmptmulf  46459  dvnmul  46465  dvmptfprodlem  46466  dvmptfprod  46467  dvnprodlem1  46468  dvnprodlem2  46469  iblsplitf  46492  itgperiod  46503  stoweidlem3  46525  stoweidlem26  46548  stoweidlem27  46549  stoweidlem29  46551  stoweidlem31  46553  stoweidlem34  46556  stoweidlem35  46557  stoweidlem36  46558  stoweidlem39  46561  stoweidlem42  46564  stoweidlem43  46565  stoweidlem44  46566  stoweidlem46  46568  stoweidlem48  46570  stoweidlem49  46571  stoweidlem51  46573  stoweidlem52  46574  stoweidlem53  46575  stoweidlem54  46576  stoweidlem55  46577  stoweidlem56  46578  stoweidlem57  46579  stoweidlem58  46580  stoweidlem59  46581  stoweidlem60  46582  stoweidlem61  46583  stoweidlem62  46584  stoweid  46585  wallispilem3  46589  stirlinglem13  46608  stirling  46611  fourierdlem16  46645  fourierdlem21  46650  fourierdlem22  46651  fourierdlem31  46660  fourierdlem39  46668  fourierdlem48  46676  fourierdlem51  46679  fourierdlem68  46696  fourierdlem71  46699  fourierdlem73  46701  fourierdlem80  46708  fourierdlem81  46709  fourierdlem86  46714  fourierdlem87  46715  fourierdlem93  46721  fourierdlem94  46722  fourierdlem103  46731  fourierdlem104  46732  fourierdlem112  46740  fourierdlem113  46741  elaa2  46756  etransclem32  46788  salexct  46856  sge0revalmpt  46900  sge0f1o  46904  sge0lefi  46920  sge0resplit  46928  sge0lempt  46932  sge0iunmptlemre  46937  sge0fodjrnlem  46938  sge0iunmpt  46940  sge0ltfirpmpt2  46948  sge0isum  46949  sge0xp  46951  sge0isummpt2  46954  sge0xadd  46957  sge0pnffsumgt  46964  sge0gtfsumgt  46965  sge0uzfsumgt  46966  sge0reuz  46969  sge0reuzb  46970  iundjiun  46982  meadjiun  46988  ismeannd  46989  voliunsge0lem  46994  meaiunincf  47005  meaiuninc3v  47006  meaiuninc3  47007  meaiininc  47009  caragenfiiuncl  47037  omeiunltfirp  47041  ovnsubaddlem2  47093  hoidmvval0  47109  hoidmvlelem1  47117  hoidmvlelem3  47119  hoidmvlelem5  47121  ovnlecvr2  47132  hspdifhsp  47138  hoiqssbllem2  47145  hoiqssbllem3  47146  hspmbllem2  47149  opnvonmbllem2  47155  hoimbl2  47187  vonhoire  47194  iinhoiicc  47196  iunhoiioolem  47197  iunhoiioo  47198  vonioo  47204  vonicc  47207  vonn0ioo2  47212  vonn0icc2  47214  salpreimagelt  47229  salpreimalegt  47231  pimincfltioc  47238  pimdecfgtioo  47239  pimincfltioo  47240  preimageiingt  47242  preimaleiinlt  47243  salpreimagtge  47247  salpreimaltle  47248  salpreimalelt  47251  salpreimagtlt  47252  incsmflem  47263  issmflelem  47266  issmfle  47267  smfconst  47271  issmfgtlem  47277  issmfgt  47278  smfaddlem2  47286  smfadd  47287  decsmflem  47288  decsmf  47289  issmfgelem  47291  issmfge  47292  smflimlem2  47294  smflim  47299  smfresal  47310  smfrec  47311  smfmullem4  47316  smfmul  47317  smfpimcc  47330  smflimmpt  47332  smfsuplem1  47333  smfsupmpt  47337  smfsupxr  47338  smfinflem  47339  smfinfmpt  47341  smflimsuplem5  47346  smflimsuplem7  47348  smflimsuplem8  47349  smflimsupmpt  47351  smfliminflem  47352  smfliminfmpt  47354  smfpimne2  47362  fsupdm  47364  smfsupdmmbllem  47366  finfdm  47368  smfinfdmmbllem  47370  or2expropbilem2  47575  or2expropbi  47576  cfsetsnfsetf  47600  2reu8i  47655  nfdfat  47669  iccelpart  47987  ichnfim  48018  ich2exprop  48025  ichreuopeq  48027  sprsymrelfo  48051  reupr  48076  reuopreuprim  48080  2zrngmmgm  48822  cbvmpox2  48906  ovmpordxf  48909  1arymaptfo  49213  2arymaptfo  49224  iinfssclem3  49625  iinfssc  49626  iinfsubc  49627  setrec1  50260  pgindnf  50285  aacllem  50370