Theorem nfan 1903

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

Syntax hints:   ∧ wa 396  ⊤wtru 1540  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfnan  1904  nf3an  1905  hban  2298  nfeqf  2382  nfald2  2446  2ax6elem  2471  nfsb4t  2504  nfeu1ALT  2590  eupicka  2637  mopick2  2640  2mo  2651  clelabOLD  2885  nfabd2  2934  2ralbida  3163  r19.12  3258  r19.12OLD  3259  ralcom2  3291  reean  3294  nfrmow  3305  nfreuw  3306  nfrabw  3319  cbvrmow  3376  cbvreuwOLD  3378  cbvreu  3382  cbvrabw  3425  cbvrab  3426  ralimda  3432  ceqsex2  3483  vtocl2gaf  3516  spc2ed  3541  rspce  3551  eqvincf  3581  elrabf  3621  elrab3t  3624  rexab2  3637  morex  3655  reu2  3661  rmo3f  3670  reu2eqd  3672  sbc2iegf  3799  reu8nf  3811  rmo2  3821  rmo3  3823  csbiebt  3863  csbie2t  3874  cbvrabcsfw  3877  cbvreucsf  3880  cbvrabcsf  3881  reusngf  4609  rexreusng  4616  reuprg0  4639  rabsnifsb  4659  nfop  4821  nfopd  4822  eluniab  4855  iuneqconst  4936  cbvopab  5147  cbvopab1  5150  cbvopab1g  5151  cbvopab2  5152  cbvopab1s  5153  mpteq12f  5163  nfmpt  5182  cbvmptf  5184  cbvmptfg  5185  axrep3  5214  axrep4  5215  axrep5  5216  reusv2lem3  5324  axprlem4  5350  axprlem5  5351  nfpo  5509  nfso  5510  nffr  5564  nfwe  5566  nfxp  5623  opeliunxp  5655  nfco  5777  elrnmpt1  5870  nfimad  5981  reuop  6200  iota2  6426  nffun  6464  imadif  6525  nffn  6541  nff  6605  nff1  6677  nffo  6696  nff1o  6723  nffvd  6795  fv3  6801  fvmptdf  6890  f1ossf1o  7009  fmptco  7010  fsnex  7164  nfiso  7202  nfriotadw  7249  cbvriotaw  7250  nfriotad  7253  cbvriota  7255  riota2df  7265  riota5f  7270  oprabv  7344  nfoprab  7348  mpoeq123  7356  nfmpo  7366  cbvoprab1  7371  cbvoprab2  7372  cbvoprab12  7373  cbvoprab3  7375  cbvmpox  7377  ovmpodxf  7432  elovmporab  7524  elovmporab1w  7525  elovmporab1  7526  onminex  7661  peano5OLD  7750  fiun  7794  f1iun  7795  opabex3d  7817  opabex3rd  7818  opabex3  7819  dfoprab4f  7905  fmpox  7916  opeliunxp2f  8035  nffrecs  8108  frrlem4  8114  nfwrecsOLD  8142  wfrlem4OLD  8152  tfr3  8239  tz7.49  8285  erovlem  8611  nfixpw  8713  nfixp  8714  nfixp1  8715  xpf1o  8935  nneneq  9001  nneneqOLD  9013  ac6sfi  9067  nfoi  9282  wdom2d  9348  infpssrlem4  10071  hsmexlem2  10192  hsmexlem4  10194  domtriomlem  10207  axdc3lem2  10216  axdc4lem  10220  zorn2lem4  10264  zorn2lem5  10265  konigthlem  10333  axextnd  10356  axrepndlem2  10358  axrepnd  10359  axunnd  10361  axpowndlem2  10363  axpowndlem4  10365  axpownd  10366  axregndlem2  10368  axregnd  10369  axinfndlem1  10370  axinfnd  10371  zfcndrep  10379  zfcndinf  10383  dedekind  11147  dedekindle  11148  fsuppmapnn0fiublem  13719  fsuppmapnn0fiub  13720  fsuppmapnn0fiubex  13721  reuccatpfxs1  14469  nfsum1  15410  nfsum  15411  nfsumOLD  15412  fsumclf  15459  fsumsplitf  15463  fsumsplit1  15466  fsum2dlem  15491  fsum00  15519  nfcprod1  15629  nfcprod  15630  fprod2dlem  15699  fprodsplitf  15707  fprodsplit1f  15709  fprodle  15715  lcmfunsnlem1  16351  lcmfunsnlem2lem1  16352  lcmfunsnlem2  16354  mreexexd  17366  acsmapd  18281  gsum2d2lem  19583  dprd2d2  19656  gsummoncoe1  21484  gsummatr01lem4  21816  cpmatmcllem  21876  cayleyhamilton1  22050  neiptopnei  22292  neiptopreu  22293  neitr  22340  iunconnlem  22587  iunconn  22588  ptcnplem  22781  ptcnp  22782  xkocnv  22974  isfildlem  23017  utopsnneiplem  23408  isucn2  23440  cfilucfil  23724  restmetu  23735  ovolfiniun  24674  ovoliunlem3  24677  ovoliunnul  24680  volfiniun  24720  itg2splitlem  24922  itg2split  24923  isibl2  24940  nfitg  24948  cbvitg  24949  limciun  25067  2sqmo  26594  2sqreulem4  26611  istrkg2ld  26830  chirred  30766  sbc2iedf  30824  rspc2daf  30825  opreu2reuALT  30834  mo5f  30846  foresf1o  30859  iinabrex  30917  cbvdisjf  30919  disjabrex  30930  disjabrexf  30931  funimass4f  30981  2ndresdju  30995  fmptcof2  31003  fcomptf  31004  acunirnmpt2  31006  acunirnmpt2f  31007  aciunf1lem  31008  funcnv4mpt  31015  fnpreimac  31017  cnvoprabOLD  31064  f1od2  31065  fpwrelmap  31077  xrofsup  31099  nn0min  31143  fprodex01  31148  fsumiunle  31152  isarchiofld  31525  nsgqusf1olem1  31607  nsgqusf1olem3  31609  elrspunidl  31615  fedgmullem2  31720  reff  31798  locfinreflem  31799  cmpcref  31809  zarclsiin  31830  zarcmplem  31840  ordtconnlem1  31883  prodindf  32000  esumcl  32007  gsumesum  32036  esumlub  32037  esumcst  32040  esumrnmpt2  32045  esumfzf  32046  esumfsup  32047  hasheuni  32062  esumcvg  32063  esumgect  32067  esumcvgre  32068  esum2dlem  32069  esum2d  32070  esumiun  32071  ldsysgenld  32137  sigapildsyslem  32138  sigapildsys  32139  ldgenpisyslem1  32140  measvunilem  32189  measvunilem0  32190  measvuni  32191  measinblem  32197  voliune  32206  volfiniune  32207  volmeas  32208  oms0  32273  omssubadd  32276  eulerpartlemgvv  32352  dstrvprob  32447  breprexplema  32619  bnj919  32756  bnj1146  32780  bnj1379  32819  bnj849  32914  bnj916  32922  bnj964  32932  bnj1014  32950  bnj1123  32975  bnj1228  33000  bnj1307  33012  bnj1321  33016  bnj1398  33023  bnj1408  33025  bnj1444  33032  bnj1445  33033  bnj1446  33034  bnj1449  33037  bnj1467  33043  bnj1463  33044  bnj1489  33045  bnj1491  33046  bnj1312  33047  bnj1525  33058  fineqvrep  33073  cvmcov  33234  iota5f  33678  axextdist  33784  axextbdist  33785  nfwlim  33825  finminlem  34516  bj-dvelimdv  35044  bj-opabco  35368  isbasisrelowllem1  35535  isbasisrelowllem2  35536  fvineqsneu  35591  fvineqsneq  35592  wl-cbvalnaed  35700  wl-2sb6d  35722  wl-sbalnae  35726  wl-mo2tf  35735  wl-eutf  35737  wl-ax11-lem3  35747  phpreu  35770  poimirlem26  35812  poimirlem27  35813  heicant  35821  mbfposadd  35833  ftc1anclem5  35863  indexdom  35901  filbcmb  35907  sdclem2  35909  sdclem1  35910  fdc1  35913  riotasv2d  36978  riotasv2s  36979  nfded2  36989  glbconxN  37399  pmapglb2xN  37793  cdlemefs32sn1aw  38435  mzpsubmpt  40572  mzpexpmpt  40574  eq0rabdioph  40605  eqrabdioph  40606  setindtr  40853  ss2iundf  41274  scottabf  41865  mnuprdlem4  41900  ismnushort  41926  binomcxplemnotnn0  41981  iunconnlem2  42562  elunif  42566  rspcegf  42573  fnchoice  42579  refsumcn  42580  rfcnnnub  42586  uzwo4  42608  fiiuncl  42620  cbvmpo2  42654  cbvmpo1  42655  iinssiin  42685  disjf1  42727  disjrnmpt2  42733  disjf1o  42736  fompt  42737  disjinfi  42738  choicefi  42747  axccdom  42769  dmrelrnrel  42772  axccd  42775  funimassd  42777  rnmptbddlem  42796  rnmptbd2lem  42801  infnsuprnmpt  42803  rnmptbdlem  42808  rnmptssbi  42814  upbdrech  42851  ssfiunibd  42855  supxrgere  42879  supxrgelem  42883  supxrge  42884  xralrple2  42900  infxr  42913  infxrunb2  42914  xrralrecnnle  42929  xrralrecnnge  42937  supxrunb3  42946  supxrleubrnmpt  42953  infleinf2  42961  unb2ltle  42962  rexabslelem  42965  suprleubrnmpt  42969  uzub  42978  supminfrnmpt  42992  supxrleubrnmptf  42998  infxrgelbrnmpt  43001  infrpgernmpt  43012  monoordxr  43030  monoord2xr  43032  iccshift  43063  iooshift  43067  iooiinicc  43087  iooiinioc  43101  fsummulc1f  43119  fsumf1of  43122  fsumreclf  43124  fsumlessf  43125  fmul01  43128  fmuldfeqlem1  43130  fmuldfeq  43131  fmul01lt1lem1  43132  fmul01lt1lem2  43133  fprodexp  43142  mccl  43146  fprodcnlem  43147  fprodcn  43148  climmulf  43152  climexp  43153  climsuse  43156  climrecf  43157  climinff  43159  climaddf  43163  mullimc  43164  islptre  43167  climf  43170  mullimcf  43171  rexlim2d  43173  idlimc  43174  limcperiod  43176  limcrecl  43177  islpcn  43187  limsupre  43189  limcleqr  43192  addlimc  43196  limclner  43199  climsubmpt  43208  climreclf  43212  climf2  43214  climeldmeqmpt  43216  clim2f2  43218  climfveqmpt  43219  fnlimfvre  43222  allbutfifvre  43223  climleltrp  43224  fnlimf  43226  fnlimabslt  43227  climfveqf  43228  climfveqmpt3  43230  climeldmeqf  43231  climeqf  43236  climeldmeqmpt3  43237  limsuppnfd  43250  limsupub  43252  climinf2lem  43254  climinf2  43255  limsuppnf  43259  limsupubuz  43261  climinf2mpt  43262  climinfmpt  43263  climinf3  43264  limsupmnflem  43268  limsupequz  43271  limsupre2  43273  limsupmnfuzlem  43274  limsupequzmptf  43279  limsupre3  43281  limsupre3uzlem  43283  limsupreuzmpt  43287  climisp  43294  lmbr3  43295  climrescn  43296  climxrrelem  43297  climxrre  43298  limsupub2  43360  liminflbuz2  43363  xlimmnfvlem2  43381  xlimmnfv  43382  xlimpnfvlem2  43385  xlimpnfv  43386  xlimmnfmpt  43391  xlimpnfmpt  43392  climxlim2lem  43393  cncficcgt0  43436  cncfioobd  43445  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  dvmptmulf  43485  dvnmul  43491  dvmptfprodlem  43492  dvmptfprod  43493  dvnprodlem1  43494  dvnprodlem2  43495  iblsplitf  43518  itgperiod  43529  stoweidlem3  43551  stoweidlem26  43574  stoweidlem27  43575  stoweidlem29  43577  stoweidlem31  43579  stoweidlem34  43582  stoweidlem35  43583  stoweidlem36  43584  stoweidlem39  43587  stoweidlem42  43590  stoweidlem43  43591  stoweidlem44  43592  stoweidlem46  43594  stoweidlem48  43596  stoweidlem49  43597  stoweidlem51  43599  stoweidlem52  43600  stoweidlem53  43601  stoweidlem54  43602  stoweidlem55  43603  stoweidlem56  43604  stoweidlem57  43605  stoweidlem58  43606  stoweidlem59  43607  stoweidlem60  43608  stoweidlem61  43609  stoweidlem62  43610  stoweid  43611  wallispilem3  43615  stirlinglem13  43634  stirling  43637  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem31  43686  fourierdlem39  43694  fourierdlem48  43702  fourierdlem51  43705  fourierdlem68  43722  fourierdlem71  43725  fourierdlem73  43727  fourierdlem80  43734  fourierdlem81  43735  fourierdlem86  43740  fourierdlem87  43741  fourierdlem93  43747  fourierdlem94  43748  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fourierdlem113  43767  elaa2  43782  etransclem32  43814  salexct  43880  sge0revalmpt  43923  sge0f1o  43927  sge0lefi  43943  sge0resplit  43951  sge0lempt  43955  sge0iunmptlemre  43960  sge0fodjrnlem  43961  sge0iunmpt  43963  sge0ltfirpmpt2  43971  sge0isum  43972  sge0xp  43974  sge0isummpt2  43977  sge0xadd  43980  sge0pnffsumgt  43987  sge0gtfsumgt  43988  sge0uzfsumgt  43989  sge0reuz  43992  sge0reuzb  43993  iundjiun  44005  meadjiun  44011  ismeannd  44012  voliunsge0lem  44017  meaiunincf  44028  meaiuninc3v  44029  meaiuninc3  44030  meaiininc  44032  caragenfiiuncl  44060  omeiunltfirp  44064  ovnsubaddlem2  44116  hoidmvval0  44132  hoidmvlelem1  44140  hoidmvlelem3  44142  hoidmvlelem5  44144  ovnlecvr2  44155  hspdifhsp  44161  hoiqssbllem2  44168  hoiqssbllem3  44169  hspmbllem2  44172  opnvonmbllem2  44178  hoimbl2  44210  vonhoire  44217  iinhoiicc  44219  iunhoiioolem  44220  iunhoiioo  44221  vonioo  44227  vonicc  44230  vonn0ioo2  44235  vonn0icc2  44237  salpreimagelt  44252  salpreimalegt  44254  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  preimageiingt  44265  preimaleiinlt  44266  salpreimagtge  44270  salpreimaltle  44271  salpreimalelt  44274  salpreimagtlt  44275  incsmflem  44286  issmflelem  44289  issmfle  44290  smfconst  44294  issmfgtlem  44300  issmfgt  44301  smfaddlem2  44309  smfadd  44310  decsmflem  44311  decsmf  44312  issmfgelem  44314  issmfge  44315  smflimlem2  44317  smflim  44322  smfresal  44333  smfrec  44334  smfmullem4  44339  smfmul  44340  smfpimcc  44352  smflimmpt  44354  smfsuplem1  44355  smfsupmpt  44359  smfsupxr  44360  smfinflem  44361  smfinfmpt  44363  smflimsuplem5  44368  smflimsuplem7  44370  smflimsuplem8  44371  smflimsupmpt  44373  smfliminflem  44374  smfliminfmpt  44376  or2expropbilem2  44538  or2expropbi  44539  cfsetsnfsetf  44563  2reu8i  44616  nfdfat  44630  iccelpart  44896  ichnfim  44927  ich2exprop  44934  ichreuopeq  44936  sprsymrelfo  44960  reupr  44985  reuopreuprim  44989  2zrngmmgm  45515  opeliun2xp  45679  cbvmpox2  45682  ovmpordxf  45685  1arymaptfo  46000  2arymaptfo  46011  setrec1  46408  aacllem  46516