Theorem nfan 1894

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

Syntax hints:   ∧ wa 395  ⊤wtru 1534  Ⅎwnf 1777

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-nf 1778

This theorem is referenced by:  nfnan  1895  nf3an  1896  hban  2288  nfeqf  2372  nfald2  2436  2ax6elem  2461  nfsb4t  2490  nfeu1ALT  2575  eupicka  2622  mopick2  2625  2mo  2636  clelabOLD  2872  nfabd2  2921  2ralbida  3272  r19.12  3303  r19.12OLD  3304  reean  3305  ralcom2  3365  cbvrmow  3397  nfrmow  3401  nfreuw  3402  cbvreuwOLD  3404  cbvreu  3416  cbvrabw  3459  nfrabw  3460  cbvrab  3465  ceqsex2  3522  vtocl2gaf  3560  spc2ed  3583  rspce  3593  eqvincf  3631  elrabf  3672  elrab3t  3675  rexab2  3688  morex  3708  reu2  3714  rmo3f  3723  reu2eqd  3725  sbc2iegf  3852  reu8nf  3864  rmo2  3874  rmo3  3876  csbiebt  3916  csbie2t  3927  cbvrabcsfw  3930  cbvreucsf  3933  cbvrabcsf  3934  reusngf  4669  rexreusng  4676  reuprg0  4699  rabsnifsb  4719  nfop  4882  nfopd  4883  eluniab  4914  iuneqconst  4999  cbvopab  5211  cbvopab1  5214  cbvopab1g  5215  cbvopab2  5216  cbvopab1s  5217  mpteq12f  5227  nfmpt  5246  cbvmptf  5248  cbvmptfg  5249  axrep3  5280  axrep4  5281  axrep5  5282  reusv2lem3  5389  axprlem4  5415  axprlem5  5416  nfpo  5584  nfso  5585  nffr  5641  nfwe  5643  nfxp  5700  opeliunxp  5734  nfco  5856  elrnmpt1  5948  nfimad  6059  reuop  6283  iota2  6523  nffun  6562  imadif  6623  nffn  6639  nff  6704  nff1  6776  nffo  6795  nff1o  6822  nffvd  6894  fv3  6900  funimassd  6949  fvmptdf  6995  fompt  7110  f1ossf1o  7119  fmptco  7120  fsnex  7274  nfiso  7312  nfriotadw  7366  cbvriotaw  7367  nfriotad  7370  cbvriota  7372  riota2df  7382  riota5f  7387  oprabv  7462  nfoprab  7466  mpoeq123  7474  nfmpo  7484  cbvoprab1  7489  cbvoprab2  7490  cbvoprab12  7491  cbvoprab3  7493  cbvmpox  7495  ovmpodxf  7551  elovmporab  7646  elovmporab1w  7647  elovmporab1  7648  onminex  7784  peano5OLD  7879  fiun  7923  f1iun  7924  opabex3d  7946  opabex3rd  7947  opabex3  7948  dfoprab4f  8036  fmpox  8047  opeliunxp2f  8191  nffrecs  8264  frrlem4  8270  nfwrecsOLD  8298  wfrlem4OLD  8308  tfr3  8395  tz7.49  8441  erovlem  8804  nfixpw  8907  nfixp  8908  nfixp1  8909  xpf1o  9136  nneneq  9206  nneneqOLD  9218  ac6sfi  9284  nfoi  9506  wdom2d  9572  infpssrlem4  10298  hsmexlem2  10419  hsmexlem4  10421  domtriomlem  10434  axdc3lem2  10443  axdc4lem  10447  zorn2lem4  10491  zorn2lem5  10492  konigthlem  10560  axextnd  10583  axrepndlem2  10585  axrepnd  10586  axunnd  10588  axpowndlem2  10590  axpowndlem4  10592  axpownd  10593  axregndlem2  10595  axregnd  10596  axinfndlem1  10597  axinfnd  10598  zfcndrep  10606  zfcndinf  10610  dedekind  11375  dedekindle  11376  fsuppmapnn0fiublem  13953  fsuppmapnn0fiub  13954  fsuppmapnn0fiubex  13955  reuccatpfxs1  14695  nfsum1  15634  nfsum  15635  fsumclf  15682  fsumsplitf  15686  fsumsplit1  15689  fsum2dlem  15714  fsum00  15742  nfcprod1  15852  nfcprod  15853  fprod2dlem  15922  fprodsplitf  15930  fprodsplit1f  15932  fprodle  15938  lcmfunsnlem1  16573  lcmfunsnlem2lem1  16574  lcmfunsnlem2  16576  mreexexd  17593  acsmapd  18511  gsum2d2lem  19885  dprd2d2  19958  gsummoncoe1  22151  gsummatr01lem4  22484  cpmatmcllem  22544  cayleyhamilton1  22718  neiptopnei  22960  neiptopreu  22961  neitr  23008  iunconnlem  23255  iunconn  23256  ptcnplem  23449  ptcnp  23450  xkocnv  23642  isfildlem  23685  utopsnneiplem  24076  isucn2  24108  cfilucfil  24392  restmetu  24403  ovolfiniun  25354  ovoliunlem3  25357  ovoliunnul  25360  volfiniun  25400  itg2splitlem  25602  itg2split  25603  isibl2  25620  nfitg  25628  cbvitg  25629  limciun  25747  2sqmo  27289  2sqreulem4  27306  istrkg2ld  28183  chirred  32120  sbc2iedf  32179  rspc2daf  32180  opreu2reuALT  32189  mo5f  32201  foresf1o  32214  iinabrex  32272  cbvdisjf  32274  disjabrex  32285  disjabrexf  32286  funimass4f  32333  2ndresdju  32346  fmptcof2  32354  fcomptf  32355  acunirnmpt2  32357  acunirnmpt2f  32358  aciunf1lem  32359  funcnv4mpt  32366  fnpreimac  32368  cnvoprabOLD  32417  f1od2  32418  fpwrelmap  32430  xrofsup  32452  nn0min  32496  fprodex01  32501  fsumiunle  32505  isarchiofld  32904  nsgqusf1olem1  32996  nsgqusf1olem3  32998  elrspunidl  33018  fedgmullem2  33197  irngnzply1  33238  reff  33311  locfinreflem  33312  cmpcref  33322  zarclsiin  33343  zarcmplem  33353  ordtconnlem1  33396  prodindf  33513  esumcl  33520  gsumesum  33549  esumlub  33550  esumcst  33553  esumrnmpt2  33558  esumfzf  33559  esumfsup  33560  hasheuni  33575  esumcvg  33576  esumgect  33580  esumcvgre  33581  esum2dlem  33582  esum2d  33583  esumiun  33584  ldsysgenld  33650  sigapildsyslem  33651  sigapildsys  33652  ldgenpisyslem1  33653  measvunilem  33702  measvunilem0  33703  measvuni  33704  measinblem  33710  voliune  33719  volfiniune  33720  volmeas  33721  oms0  33788  omssubadd  33791  eulerpartlemgvv  33867  dstrvprob  33962  breprexplema  34133  bnj919  34269  bnj1146  34293  bnj1379  34332  bnj849  34427  bnj916  34435  bnj964  34445  bnj1014  34463  bnj1123  34488  bnj1228  34513  bnj1307  34525  bnj1321  34529  bnj1398  34536  bnj1408  34538  bnj1444  34545  bnj1445  34546  bnj1446  34547  bnj1449  34550  bnj1467  34556  bnj1463  34557  bnj1489  34558  bnj1491  34559  bnj1312  34560  bnj1525  34571  fineqvrep  34586  cvmcov  34745  iota5f  35190  axextdist  35267  axextbdist  35268  nfwlim  35290  finminlem  35694  bj-dvelimdv  36221  bj-opabco  36560  isbasisrelowllem1  36727  isbasisrelowllem2  36728  fvineqsneu  36783  fvineqsneq  36784  wl-cbvalnaed  36892  wl-2sb6d  36917  wl-sbalnae  36921  wl-mo2tf  36930  wl-eutf  36932  wl-ax11-lem3  36943  phpreu  36966  poimirlem26  37008  poimirlem27  37009  heicant  37017  mbfposadd  37029  ftc1anclem5  37059  indexdom  37096  filbcmb  37102  sdclem2  37104  sdclem1  37105  fdc1  37108  riotasv2d  38321  riotasv2s  38322  nfded2  38332  glbconxN  38743  pmapglb2xN  39137  cdlemefs32sn1aw  39779  mzpsubmpt  41995  mzpexpmpt  41997  eq0rabdioph  42028  eqrabdioph  42029  setindtr  42277  unielss  42481  nadd1suc  42656  naddsuc2  42657  ss2iundf  42924  scottabf  43513  mnuprdlem4  43548  ismnushort  43574  binomcxplemnotnn0  43629  iunconnlem2  44210  elunif  44214  rspcegf  44221  fnchoice  44227  refsumcn  44228  rfcnnnub  44234  uzwo4  44253  fiiuncl  44265  cbvmpo2  44299  cbvmpo1  44300  iinssiin  44331  disjf1  44392  disjrnmpt2  44397  disjf1o  44400  disjinfi  44401  choicefi  44409  axccdom  44431  dmrelrnrel  44435  axccd  44438  rnmptbddlem  44458  rnmptbd2lem  44462  infnsuprnmpt  44464  rnmptbdlem  44469  rnmptssbi  44475  upbdrech  44525  ssfiunibd  44529  supxrgere  44553  supxrgelem  44557  supxrge  44558  xralrple2  44574  infxr  44587  infxrunb2  44588  xrralrecnnle  44603  xrralrecnnge  44610  supxrunb3  44619  supxrleubrnmpt  44626  infleinf2  44634  unb2ltle  44635  rexabslelem  44638  suprleubrnmpt  44642  uzub  44651  supminfrnmpt  44665  supxrleubrnmptf  44671  infxrgelbrnmpt  44674  infrpgernmpt  44685  monoordxr  44703  monoord2xr  44705  caucvgbf  44710  cvgcaule  44712  iccshift  44741  iooshift  44745  iooiinicc  44765  iooiinioc  44779  fsummulc1f  44797  fsumf1of  44800  fsumreclf  44802  fsumlessf  44803  fmul01  44806  fmuldfeqlem1  44808  fmuldfeq  44809  fmul01lt1lem1  44810  fmul01lt1lem2  44811  fprodexp  44820  mccl  44824  fprodcnlem  44825  fprodcn  44826  climmulf  44830  climexp  44831  climsuse  44834  climrecf  44835  climinff  44837  climaddf  44841  mullimc  44842  islptre  44845  climf  44848  mullimcf  44849  rexlim2d  44851  idlimc  44852  limcperiod  44854  limcrecl  44855  islpcn  44865  limsupre  44867  limcleqr  44870  addlimc  44874  limclner  44877  climsubmpt  44886  climreclf  44890  climf2  44892  climeldmeqmpt  44894  clim2f2  44896  climfveqmpt  44897  fnlimfvre  44900  allbutfifvre  44901  climleltrp  44902  fnlimf  44904  fnlimabslt  44905  climfveqf  44906  climfveqmpt3  44908  climeldmeqf  44909  climeqf  44914  climeldmeqmpt3  44915  limsuppnfd  44928  limsupub  44930  climinf2lem  44932  climinf2  44933  limsuppnf  44937  limsupubuz  44939  climinf2mpt  44940  climinfmpt  44941  climinf3  44942  limsupmnflem  44946  limsupequz  44949  limsupre2  44951  limsupmnfuzlem  44952  limsupequzmptf  44957  limsupre3  44959  limsupre3uzlem  44961  limsupreuzmpt  44965  climisp  44972  lmbr3  44973  climrescn  44974  climxrrelem  44975  climxrre  44976  limsupub2  45038  liminflbuz2  45041  xlimmnfvlem2  45059  xlimmnfv  45060  xlimpnfvlem2  45063  xlimpnfv  45064  xlimmnfmpt  45069  xlimpnfmpt  45070  climxlim2lem  45071  cncficcgt0  45114  cncfioobd  45123  fprodsubrecnncnvlem  45133  fprodaddrecnncnvlem  45135  dvmptmulf  45163  dvnmul  45169  dvmptfprodlem  45170  dvmptfprod  45171  dvnprodlem1  45172  dvnprodlem2  45173  iblsplitf  45196  itgperiod  45207  stoweidlem3  45229  stoweidlem26  45252  stoweidlem27  45253  stoweidlem29  45255  stoweidlem31  45257  stoweidlem34  45260  stoweidlem35  45261  stoweidlem36  45262  stoweidlem39  45265  stoweidlem42  45268  stoweidlem43  45269  stoweidlem44  45270  stoweidlem46  45272  stoweidlem48  45274  stoweidlem49  45275  stoweidlem51  45277  stoweidlem52  45278  stoweidlem53  45279  stoweidlem54  45280  stoweidlem55  45281  stoweidlem56  45282  stoweidlem57  45283  stoweidlem58  45284  stoweidlem59  45285  stoweidlem60  45286  stoweidlem61  45287  stoweidlem62  45288  stoweid  45289  wallispilem3  45293  stirlinglem13  45312  stirling  45315  fourierdlem16  45349  fourierdlem21  45354  fourierdlem22  45355  fourierdlem31  45364  fourierdlem39  45372  fourierdlem48  45380  fourierdlem51  45383  fourierdlem68  45400  fourierdlem71  45403  fourierdlem73  45405  fourierdlem80  45412  fourierdlem81  45413  fourierdlem86  45418  fourierdlem87  45419  fourierdlem93  45425  fourierdlem94  45426  fourierdlem103  45435  fourierdlem104  45436  fourierdlem112  45444  fourierdlem113  45445  elaa2  45460  etransclem32  45492  salexct  45560  sge0revalmpt  45604  sge0f1o  45608  sge0lefi  45624  sge0resplit  45632  sge0lempt  45636  sge0iunmptlemre  45641  sge0fodjrnlem  45642  sge0iunmpt  45644  sge0ltfirpmpt2  45652  sge0isum  45653  sge0xp  45655  sge0isummpt2  45658  sge0xadd  45661  sge0pnffsumgt  45668  sge0gtfsumgt  45669  sge0uzfsumgt  45670  sge0reuz  45673  sge0reuzb  45674  iundjiun  45686  meadjiun  45692  ismeannd  45693  voliunsge0lem  45698  meaiunincf  45709  meaiuninc3v  45710  meaiuninc3  45711  meaiininc  45713  caragenfiiuncl  45741  omeiunltfirp  45745  ovnsubaddlem2  45797  hoidmvval0  45813  hoidmvlelem1  45821  hoidmvlelem3  45823  hoidmvlelem5  45825  ovnlecvr2  45836  hspdifhsp  45842  hoiqssbllem2  45849  hoiqssbllem3  45850  hspmbllem2  45853  opnvonmbllem2  45859  hoimbl2  45891  vonhoire  45898  iinhoiicc  45900  iunhoiioolem  45901  iunhoiioo  45902  vonioo  45908  vonicc  45911  vonn0ioo2  45916  vonn0icc2  45918  salpreimagelt  45933  salpreimalegt  45935  pimincfltioc  45942  pimdecfgtioo  45943  pimincfltioo  45944  preimageiingt  45946  preimaleiinlt  45947  salpreimagtge  45951  salpreimaltle  45952  salpreimalelt  45955  salpreimagtlt  45956  incsmflem  45967  issmflelem  45970  issmfle  45971  smfconst  45975  issmfgtlem  45981  issmfgt  45982  smfaddlem2  45990  smfadd  45991  decsmflem  45992  decsmf  45993  issmfgelem  45995  issmfge  45996  smflimlem2  45998  smflim  46003  smfresal  46014  smfrec  46015  smfmullem4  46020  smfmul  46021  smfpimcc  46034  smflimmpt  46036  smfsuplem1  46037  smfsupmpt  46041  smfsupxr  46042  smfinflem  46043  smfinfmpt  46045  smflimsuplem5  46050  smflimsuplem7  46052  smflimsuplem8  46053  smflimsupmpt  46055  smfliminflem  46056  smfliminfmpt  46058  smfpimne2  46066  fsupdm  46068  smfsupdmmbllem  46070  finfdm  46072  smfinfdmmbllem  46074  or2expropbilem2  46253  or2expropbi  46254  cfsetsnfsetf  46278  2reu8i  46331  nfdfat  46345  iccelpart  46611  ichnfim  46642  ich2exprop  46649  ichreuopeq  46651  sprsymrelfo  46675  reupr  46700  reuopreuprim  46704  2zrngmmgm  47140  opeliun2xp  47222  cbvmpox2  47225  ovmpordxf  47228  1arymaptfo  47542  2arymaptfo  47553  setrec1  47948  pgindnf  47973  aacllem  48060