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 1548	1 ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 395  ⊤wtru 1542  Ⅎ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 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnan  1901  nf3an  1902  hban  2301  nfeqf  2380  nfald2  2444  2ax6elem  2469  nfsb4t  2498  nfeu1ALT  2583  eupicka  2628  mopick2  2631  2mo  2642  nfabd2  2916  2ralbida  3253  r19.12  3279  reean  3280  ralcom2  3341  cbvrmow  3369  nfrmow  3373  nfreuw  3374  cbvreu  3385  cbvrabw  3428  cbvrabwOLD  3429  nfrabw  3430  cbvrab  3433  ceqsex2  3488  vtocl2gafOLD  3533  vtocl3gaf  3534  spc2ed  3554  rspce  3564  eqvincf  3603  elrabf  3642  elrab3t  3644  rexab2  3656  morex  3676  reu2  3682  rmo3f  3691  reu2eqd  3693  sbc2iegf  3814  reu8nf  3826  rmo2  3836  rmo3  3838  csbiebt  3877  csbie2t  3886  cbvrabcsfw  3889  cbvreucsf  3892  cbvrabcsf  3893  nfdif  4077  nfin  4172  reusngf  4625  rexreusng  4630  reuprg0  4653  rabsnifsb  4673  nfop  4839  nfopd  4840  eluniab  4871  iuneqconst  4951  cbvopab  5161  cbvopab1  5163  cbvopab1g  5164  cbvopab2  5165  cbvopab1s  5166  mpteq12f  5174  nfmpt  5187  cbvmptf  5189  cbvmptfg  5190  axrep3  5219  axrep4OLD  5222  axrep5  5223  reusv2lem3  5336  axprlem4OLD  5365  axprlem5OLD  5366  nfpo  5528  nfso  5529  nffr  5587  nfwe  5589  nfxp  5647  opeliunxp  5681  opeliun2xp  5682  nfco  5803  elrnmpt1  5897  nfimad  6015  reuop  6236  iota2  6466  nffun  6500  imadif  6561  nffn  6576  nff  6643  nff1  6713  nffo  6730  nff1o  6757  nffvd  6829  fv3  6835  funimassd  6883  fvmptdf  6930  fompt  7046  f1ossf1o  7056  fmptco  7057  fsnex  7212  nfiso  7251  nfriotadw  7306  cbvriotaw  7307  nfriotad  7309  cbvriota  7311  riota2df  7321  riota5f  7326  oprabv  7401  nfoprab  7405  mpoeq123  7413  nfmpo  7423  cbvoprab1  7428  cbvoprab2  7429  cbvoprab12  7430  cbvoprab3  7432  cbvmpox  7434  ovmpodxf  7491  elovmporab  7587  elovmporab1w  7588  elovmporab1  7589  onminex  7730  fiun  7870  f1iun  7871  opabex3d  7892  opabex3rd  7893  opabex3  7894  dfoprab4f  7983  fmpox  7994  opeliunxp2f  8135  nffrecs  8208  frrlem4  8214  tfr3  8313  tz7.49  8359  naddsuc2  8611  erovlem  8732  nfixpw  8835  nfixp  8836  nfixp1  8837  xpf1o  9047  nneneq  9110  ac6sfi  9163  nfoi  9395  wdom2d  9461  infpssrlem4  10189  hsmexlem2  10310  hsmexlem4  10312  domtriomlem  10325  axdc3lem2  10334  axdc4lem  10338  zorn2lem4  10382  zorn2lem5  10383  konigthlem  10451  axextnd  10474  axrepndlem2  10476  axrepnd  10477  axunnd  10479  axpowndlem2  10481  axpowndlem4  10483  axpownd  10484  axregndlem2  10486  axregnd  10487  axinfndlem1  10488  axinfnd  10489  zfcndrep  10497  zfcndinf  10501  dedekind  11268  dedekindle  11269  fsuppmapnn0fiublem  13889  fsuppmapnn0fiub  13890  fsuppmapnn0fiubex  13891  reuccatpfxs1  14646  nfsum1  15589  nfsum  15590  fsumclf  15637  fsumsplitf  15641  fsumsplit1  15644  fsum2dlem  15669  fsum00  15697  nfcprod1  15807  nfcprod  15808  fprod2dlem  15879  fprodsplitf  15887  fprodsplit1f  15889  fprodle  15895  lcmfunsnlem1  16540  lcmfunsnlem2lem1  16541  lcmfunsnlem2  16543  mreexexd  17546  acsmapd  18452  gsum2d2lem  19878  dprd2d2  19951  gsummoncoe1  22216  gsummatr01lem4  22566  cpmatmcllem  22626  cayleyhamilton1  22800  neiptopnei  23040  neiptopreu  23041  neitr  23088  iunconnlem  23335  iunconn  23336  ptcnplem  23529  ptcnp  23530  xkocnv  23722  isfildlem  23765  utopsnneiplem  24155  isucn2  24186  cfilucfil  24467  restmetu  24478  ovolfiniun  25422  ovoliunlem3  25425  ovoliunnul  25428  volfiniun  25468  itg2splitlem  25669  itg2split  25670  isibl2  25687  nfitg  25696  cbvitg  25697  limciun  25815  2sqmo  27368  2sqreulem4  27385  istrkg2ld  28431  chirred  32365  sbc2iedf  32434  rspc2daf  32435  opreu2reuALT  32446  mo5f  32458  foresf1o  32474  iinabrex  32539  cbvdisjf  32541  disjabrex  32552  disjabrexf  32553  funimass4f  32609  2ndresdju  32621  fmptcof2  32629  fcomptf  32630  acunirnmpt2  32632  acunirnmpt2f  32633  aciunf1lem  32634  funcnv4mpt  32641  fnpreimac  32643  f1od2  32692  fpwrelmap  32706  xrofsup  32740  nn0min  32793  fprodex01  32798  fsumiunle  32802  prodindf  32834  isarchiofld  33158  elrgspnsubrunlem2  33205  nsgqusf1olem1  33368  nsgqusf1olem3  33370  elrspunidl  33383  mplvrpmga  33565  fedgmullem2  33633  irngnzply1  33694  reff  33842  locfinreflem  33843  cmpcref  33853  zarclsiin  33874  zarcmplem  33884  ordtconnlem1  33927  esumcl  34033  gsumesum  34062  esumlub  34063  esumcst  34066  esumrnmpt2  34071  esumfzf  34072  esumfsup  34073  hasheuni  34088  esumcvg  34089  esumgect  34093  esumcvgre  34094  esum2dlem  34095  esum2d  34096  esumiun  34097  ldsysgenld  34163  sigapildsyslem  34164  sigapildsys  34165  ldgenpisyslem1  34166  measvunilem  34215  measvunilem0  34216  measvuni  34217  measinblem  34223  voliune  34232  volfiniune  34233  volmeas  34234  oms0  34300  omssubadd  34303  eulerpartlemgvv  34379  dstrvprob  34475  breprexplema  34633  bnj919  34769  bnj1146  34793  bnj1379  34832  bnj849  34927  bnj916  34935  bnj964  34945  bnj1014  34963  bnj1123  34988  bnj1228  35013  bnj1307  35025  bnj1321  35029  bnj1398  35036  bnj1408  35038  bnj1444  35045  bnj1445  35046  bnj1446  35047  bnj1449  35050  bnj1467  35056  bnj1463  35057  bnj1489  35058  bnj1491  35059  bnj1312  35060  bnj1525  35071  dvelimalcased  35077  dvelimexcased  35079  fineqvrep  35105  cvmcov  35275  iota5f  35736  axextdist  35812  axextbdist  35813  nfwlim  35835  finminlem  36331  bj-dvelimdv  36864  bj-opabco  37201  isbasisrelowllem1  37368  isbasisrelowllem2  37369  fvineqsneu  37424  fvineqsneq  37425  wl-cbvalnaed  37545  wl-2sb6d  37571  wl-sbalnae  37575  wl-mo2tf  37584  wl-eutf  37586  wl-ax11-lem3  37600  phpreu  37623  poimirlem26  37665  poimirlem27  37666  heicant  37674  mbfposadd  37686  ftc1anclem5  37716  indexdom  37753  filbcmb  37759  sdclem2  37761  sdclem1  37762  fdc1  37765  riotasv2d  38975  riotasv2s  38976  nfded2  38986  glbconxN  39396  pmapglb2xN  39790  cdlemefs32sn1aw  40432  mzpsubmpt  42755  mzpexpmpt  42757  eq0rabdioph  42788  eqrabdioph  42789  setindtr  43036  unielss  43230  nadd1suc  43404  ss2iundf  43671  scottabf  44252  mnuprdlem4  44287  ismnushort  44313  binomcxplemnotnn0  44368  iunconnlem2  44946  nfrelp  44961  modelaxreplem3  44992  modelaxrep  44993  permaxrep  45018  elunif  45032  rspcegf  45039  fnchoice  45045  refsumcn  45046  rfcnnnub  45052  uzwo4  45069  fiiuncl  45081  cbvmpo2  45113  cbvmpo1  45114  iinssiin  45145  disjf1  45199  disjrnmpt2  45204  disjf1o  45207  disjinfi  45208  choicefi  45216  axccdom  45238  dmrelrnrel  45242  axccd  45245  rnmptbddlem  45260  rnmptbd2lem  45264  infnsuprnmpt  45266  rnmptbdlem  45271  rnmptssbi  45276  upbdrech  45325  ssfiunibd  45329  supxrgere  45351  supxrgelem  45355  supxrge  45356  xralrple2  45372  infxr  45384  infxrunb2  45385  xrralrecnnle  45400  xrralrecnnge  45407  supxrunb3  45416  supxrleubrnmpt  45423  infleinf2  45431  unb2ltle  45432  rexabslelem  45435  suprleubrnmpt  45439  uzub  45448  supminfrnmpt  45462  supxrleubrnmptf  45468  infxrgelbrnmpt  45471  infrpgernmpt  45482  monoordxr  45499  monoord2xr  45501  caucvgbf  45506  cvgcaule  45508  iccshift  45537  iooshift  45541  iooiinicc  45561  iooiinioc  45575  fsummulc1f  45590  fsumf1of  45593  fsumreclf  45595  fsumlessf  45596  fmul01  45599  fmuldfeqlem1  45601  fmuldfeq  45602  fmul01lt1lem1  45603  fmul01lt1lem2  45604  fprodexp  45613  mccl  45617  fprodcnlem  45618  fprodcn  45619  climmulf  45623  climexp  45624  climsuse  45627  climrecf  45628  climinff  45630  climaddf  45634  mullimc  45635  islptre  45638  climf  45641  mullimcf  45642  rexlim2d  45644  idlimc  45645  limcperiod  45647  limcrecl  45648  islpcn  45656  limsupre  45658  limcleqr  45661  addlimc  45665  limclner  45668  climsubmpt  45677  climreclf  45681  climf2  45683  climeldmeqmpt  45685  clim2f2  45687  climfveqmpt  45688  fnlimfvre  45691  allbutfifvre  45692  climleltrp  45693  fnlimf  45695  fnlimabslt  45696  climfveqf  45697  climfveqmpt3  45699  climeldmeqf  45700  climeqf  45705  climeldmeqmpt3  45706  limsuppnfd  45719  limsupub  45721  climinf2lem  45723  climinf2  45724  limsuppnf  45728  limsupubuz  45730  climinf2mpt  45731  climinfmpt  45732  climinf3  45733  limsupmnflem  45737  limsupequz  45740  limsupre2  45742  limsupmnfuzlem  45743  limsupequzmptf  45748  limsupre3  45750  limsupre3uzlem  45752  limsupreuzmpt  45756  climisp  45763  lmbr3  45764  climrescn  45765  climxrrelem  45766  climxrre  45767  limsupub2  45829  liminflbuz2  45832  xlimmnfvlem2  45850  xlimmnfv  45851  xlimpnfvlem2  45854  xlimpnfv  45855  xlimmnfmpt  45860  xlimpnfmpt  45861  climxlim2lem  45862  cncficcgt0  45905  cncfioobd  45914  fprodsubrecnncnvlem  45924  fprodaddrecnncnvlem  45926  dvmptmulf  45954  dvnmul  45960  dvmptfprodlem  45961  dvmptfprod  45962  dvnprodlem1  45963  dvnprodlem2  45964  iblsplitf  45987  itgperiod  45998  stoweidlem3  46020  stoweidlem26  46043  stoweidlem27  46044  stoweidlem29  46046  stoweidlem31  46048  stoweidlem34  46051  stoweidlem35  46052  stoweidlem36  46053  stoweidlem39  46056  stoweidlem42  46059  stoweidlem43  46060  stoweidlem44  46061  stoweidlem46  46063  stoweidlem48  46065  stoweidlem49  46066  stoweidlem51  46068  stoweidlem52  46069  stoweidlem53  46070  stoweidlem54  46071  stoweidlem55  46072  stoweidlem56  46073  stoweidlem57  46074  stoweidlem58  46075  stoweidlem59  46076  stoweidlem60  46077  stoweidlem61  46078  stoweidlem62  46079  stoweid  46080  wallispilem3  46084  stirlinglem13  46103  stirling  46106  fourierdlem16  46140  fourierdlem21  46145  fourierdlem22  46146  fourierdlem31  46155  fourierdlem39  46163  fourierdlem48  46171  fourierdlem51  46174  fourierdlem68  46191  fourierdlem71  46194  fourierdlem73  46196  fourierdlem80  46203  fourierdlem81  46204  fourierdlem86  46209  fourierdlem87  46210  fourierdlem93  46216  fourierdlem94  46217  fourierdlem103  46226  fourierdlem104  46227  fourierdlem112  46235  fourierdlem113  46236  elaa2  46251  etransclem32  46283  salexct  46351  sge0revalmpt  46395  sge0f1o  46399  sge0lefi  46415  sge0resplit  46423  sge0lempt  46427  sge0iunmptlemre  46432  sge0fodjrnlem  46433  sge0iunmpt  46435  sge0ltfirpmpt2  46443  sge0isum  46444  sge0xp  46446  sge0isummpt2  46449  sge0xadd  46452  sge0pnffsumgt  46459  sge0gtfsumgt  46460  sge0uzfsumgt  46461  sge0reuz  46464  sge0reuzb  46465  iundjiun  46477  meadjiun  46483  ismeannd  46484  voliunsge0lem  46489  meaiunincf  46500  meaiuninc3v  46501  meaiuninc3  46502  meaiininc  46504  caragenfiiuncl  46532  omeiunltfirp  46536  ovnsubaddlem2  46588  hoidmvval0  46604  hoidmvlelem1  46612  hoidmvlelem3  46614  hoidmvlelem5  46616  ovnlecvr2  46627  hspdifhsp  46633  hoiqssbllem2  46640  hoiqssbllem3  46641  hspmbllem2  46644  opnvonmbllem2  46650  hoimbl2  46682  vonhoire  46689  iinhoiicc  46691  iunhoiioolem  46692  iunhoiioo  46693  vonioo  46699  vonicc  46702  vonn0ioo2  46707  vonn0icc2  46709  salpreimagelt  46724  salpreimalegt  46726  pimincfltioc  46733  pimdecfgtioo  46734  pimincfltioo  46735  preimageiingt  46737  preimaleiinlt  46738  salpreimagtge  46742  salpreimaltle  46743  salpreimalelt  46746  salpreimagtlt  46747  incsmflem  46758  issmflelem  46761  issmfle  46762  smfconst  46766  issmfgtlem  46772  issmfgt  46773  smfaddlem2  46781  smfadd  46782  decsmflem  46783  decsmf  46784  issmfgelem  46786  issmfge  46787  smflimlem2  46789  smflim  46794  smfresal  46805  smfrec  46806  smfmullem4  46811  smfmul  46812  smfpimcc  46825  smflimmpt  46827  smfsuplem1  46828  smfsupmpt  46832  smfsupxr  46833  smfinflem  46834  smfinfmpt  46836  smflimsuplem5  46841  smflimsuplem7  46843  smflimsuplem8  46844  smflimsupmpt  46846  smfliminflem  46847  smfliminfmpt  46849  smfpimne2  46857  fsupdm  46859  smfsupdmmbllem  46861  finfdm  46863  smfinfdmmbllem  46865  or2expropbilem2  47043  or2expropbi  47044  cfsetsnfsetf  47068  2reu8i  47123  nfdfat  47137  iccelpart  47443  ichnfim  47474  ich2exprop  47481  ichreuopeq  47483  sprsymrelfo  47507  reupr  47532  reuopreuprim  47536  2zrngmmgm  48262  cbvmpox2  48346  ovmpordxf  48349  1arymaptfo  48654  2arymaptfo  48665  iinfssclem3  49067  iinfssc  49068  iinfsubc  49069  setrec1  49702  pgindnf  49727  aacllem  49812