Theorem nfan 1907

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

Syntax hints:   ∧ wa 399  ⊤wtru 1544  Ⅎwnf 1791

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfnan  1908  nf3an  1909  hban  2301  nfeqf  2380  nfald2  2444  2ax6elem  2469  nfsb4t  2502  nfeu1ALT  2588  eupicka  2635  mopick2  2638  2mo  2649  clelabOLD  2881  nfabd2  2930  2ralbida  3155  r19.12  3243  ralcom2  3275  reean  3278  cbvreuw  3351  cbvrmow  3352  cbvreu  3356  cbvrabw  3400  cbvrab  3401  ralimda  3407  ceqsex2  3458  vtocl2gaf  3491  spc2ed  3516  rspce  3526  eqvincf  3557  elrabf  3598  elrab3t  3601  rexab2  3613  rexab2OLD  3614  morex  3632  reu2  3638  rmo3f  3647  reu2eqd  3649  sbc2iegf  3777  reu8nf  3789  rmo2  3799  rmo3  3801  csbiebt  3841  csbie2t  3852  cbvrabcsfw  3855  cbvreucsf  3858  cbvrabcsf  3859  reusngf  4588  rexreusng  4595  reuprg0  4618  rabsnifsb  4638  nfop  4800  nfopd  4801  eluniab  4834  iuneqconst  4915  cbvopab  5125  cbvopab1  5128  cbvopab1g  5129  cbvopab2  5130  cbvopab1s  5131  mpteq12f  5138  nfmpt  5152  cbvmptf  5154  cbvmptfg  5155  axrep3  5183  axrep4  5184  axrep5  5185  reusv2lem3  5293  axprlem4  5319  axprlem5  5320  nfpo  5473  nfso  5474  nffr  5525  nfwe  5527  nfxp  5584  opeliunxp  5616  nfco  5734  elrnmpt1  5827  nfimad  5938  reuop  6156  iota2  6369  nffun  6403  imadif  6464  nffn  6478  nff  6541  nff1  6613  nffo  6632  nff1o  6659  nffvd  6729  fv3  6735  fvmptdf  6824  f1ossf1o  6943  fmptco  6944  fsnex  7093  nfiso  7131  nfriotadw  7178  cbvriotaw  7179  nfriotad  7182  cbvriota  7184  riota2df  7194  riota5f  7199  oprabv  7271  nfoprab  7275  mpoeq123  7283  nfmpo  7293  cbvoprab1  7298  cbvoprab2  7299  cbvoprab12  7300  cbvoprab3  7302  cbvmpox  7304  ovmpodxf  7359  elovmporab  7451  elovmporab1w  7452  elovmporab1  7453  onminex  7586  peano5OLD  7672  fiun  7716  f1iun  7717  opabex3d  7738  opabex3rd  7739  opabex3  7740  dfoprab4f  7826  fmpox  7837  opeliunxp2f  7952  nffrecs  8025  frrlem4  8030  nfwrecs  8049  wfrlem4  8058  tfr3  8135  tz7.49  8181  erovlem  8495  nfixpw  8597  nfixp  8598  nfixp1  8599  xpf1o  8808  nneneq  8829  ac6sfi  8915  nfoi  9130  wdom2d  9196  trpredmintr  9336  infpssrlem4  9920  hsmexlem2  10041  hsmexlem4  10043  domtriomlem  10056  axdc3lem2  10065  axdc4lem  10069  zorn2lem4  10113  zorn2lem5  10114  konigthlem  10182  axextnd  10205  axrepndlem2  10207  axrepnd  10208  axunnd  10210  axpowndlem2  10212  axpowndlem4  10214  axpownd  10215  axregndlem2  10217  axregnd  10218  axinfndlem1  10219  axinfnd  10220  zfcndrep  10228  zfcndinf  10232  dedekind  10995  dedekindle  10996  fsuppmapnn0fiublem  13563  fsuppmapnn0fiub  13564  fsuppmapnn0fiubex  13565  reuccatpfxs1  14312  nfsum1  15253  nfsum  15254  nfsumOLD  15255  fsumclf  15302  fsumsplitf  15306  fsumsplit1  15309  fsum2dlem  15334  fsum00  15362  nfcprod1  15472  nfcprod  15473  fprod2dlem  15542  fprodsplitf  15550  fprodsplit1f  15552  fprodle  15558  lcmfunsnlem1  16194  lcmfunsnlem2lem1  16195  lcmfunsnlem2  16197  mreexexd  17151  acsmapd  18060  gsum2d2lem  19358  dprd2d2  19431  gsummoncoe1  21225  gsummatr01lem4  21555  cpmatmcllem  21615  cayleyhamilton1  21789  neiptopnei  22029  neiptopreu  22030  neitr  22077  iunconnlem  22324  iunconn  22325  ptcnplem  22518  ptcnp  22519  xkocnv  22711  isfildlem  22754  utopsnneiplem  23145  isucn2  23176  cfilucfil  23457  restmetu  23468  ovolfiniun  24398  ovoliunlem3  24401  ovoliunnul  24404  volfiniun  24444  itg2splitlem  24646  itg2split  24647  isibl2  24664  nfitg  24672  cbvitg  24673  limciun  24791  2sqmo  26318  2sqreulem4  26335  istrkg2ld  26551  chirred  30476  sbc2iedf  30534  rspc2daf  30535  opreu2reuALT  30544  mo5f  30556  foresf1o  30569  iinabrex  30627  cbvdisjf  30629  disjabrex  30640  disjabrexf  30641  funimass4f  30691  2ndresdju  30705  fmptcof2  30714  fcomptf  30715  acunirnmpt2  30717  acunirnmpt2f  30718  aciunf1lem  30719  funcnv4mpt  30726  fnpreimac  30728  cnvoprabOLD  30775  f1od2  30776  fpwrelmap  30788  xrofsup  30810  nn0min  30854  fprodex01  30859  fsumiunle  30863  isarchiofld  31235  nsgqusf1olem1  31312  nsgqusf1olem3  31314  elrspunidl  31320  fedgmullem2  31425  reff  31503  locfinreflem  31504  cmpcref  31514  zarclsiin  31535  zarcmplem  31545  ordtconnlem1  31588  prodindf  31703  esumcl  31710  gsumesum  31739  esumlub  31740  esumcst  31743  esumrnmpt2  31748  esumfzf  31749  esumfsup  31750  hasheuni  31765  esumcvg  31766  esumgect  31770  esumcvgre  31771  esum2dlem  31772  esum2d  31773  esumiun  31774  ldsysgenld  31840  sigapildsyslem  31841  sigapildsys  31842  ldgenpisyslem1  31843  measvunilem  31892  measvunilem0  31893  measvuni  31894  measinblem  31900  voliune  31909  volfiniune  31910  volmeas  31911  oms0  31976  omssubadd  31979  eulerpartlemgvv  32055  dstrvprob  32150  breprexplema  32322  bnj919  32459  bnj1146  32484  bnj1379  32523  bnj849  32618  bnj916  32626  bnj964  32636  bnj1014  32654  bnj1123  32679  bnj1228  32704  bnj1307  32716  bnj1321  32720  bnj1398  32727  bnj1408  32729  bnj1444  32736  bnj1445  32737  bnj1446  32738  bnj1449  32741  bnj1467  32747  bnj1463  32748  bnj1489  32749  bnj1491  32750  bnj1312  32751  bnj1525  32762  fineqvrep  32777  cvmcov  32938  iota5f  33384  axextdist  33494  axextbdist  33495  nfwlim  33553  finminlem  34244  bj-dvelimdv  34772  bj-opabco  35094  isbasisrelowllem1  35263  isbasisrelowllem2  35264  fvineqsneu  35319  fvineqsneq  35320  wl-cbvalnaed  35428  wl-2sb6d  35450  wl-sbalnae  35454  wl-mo2tf  35463  wl-eutf  35465  wl-ax11-lem3  35475  phpreu  35498  poimirlem26  35540  poimirlem27  35541  heicant  35549  mbfposadd  35561  ftc1anclem5  35591  indexdom  35629  filbcmb  35635  sdclem2  35637  sdclem1  35638  fdc1  35641  riotasv2d  36708  riotasv2s  36709  nfded2  36719  glbconxN  37129  pmapglb2xN  37523  cdlemefs32sn1aw  38165  mzpsubmpt  40268  mzpexpmpt  40270  eq0rabdioph  40301  eqrabdioph  40302  setindtr  40549  ss2iundf  40944  scottabf  41531  mnuprdlem4  41566  ismnushort  41592  binomcxplemnotnn0  41647  iunconnlem2  42228  elunif  42232  rspcegf  42239  fnchoice  42245  refsumcn  42246  rfcnnnub  42252  uzwo4  42274  fiiuncl  42286  cbvmpo2  42320  cbvmpo1  42321  iinssiin  42351  disjf1  42393  disjrnmpt2  42399  disjf1o  42402  fompt  42403  disjinfi  42404  choicefi  42413  axccdom  42435  dmrelrnrel  42438  axccd  42441  funimassd  42443  rnmptbddlem  42461  rnmptbd2lem  42466  infnsuprnmpt  42468  rnmptbdlem  42473  rnmptssbi  42479  upbdrech  42517  ssfiunibd  42521  supxrgere  42545  supxrgelem  42549  supxrge  42550  xralrple2  42566  infxr  42579  infxrunb2  42580  xrralrecnnle  42595  xrralrecnnge  42603  supxrunb3  42612  supxrleubrnmpt  42619  infleinf2  42627  unb2ltle  42628  rexabslelem  42631  suprleubrnmpt  42635  uzub  42644  supminfrnmpt  42658  supxrleubrnmptf  42666  infxrgelbrnmpt  42669  infrpgernmpt  42680  monoordxr  42698  monoord2xr  42700  iccshift  42731  iooshift  42735  iooiinicc  42755  iooiinioc  42769  fsummulc1f  42787  fsumf1of  42790  fsumreclf  42792  fsumlessf  42793  fmul01  42796  fmuldfeqlem1  42798  fmuldfeq  42799  fmul01lt1lem1  42800  fmul01lt1lem2  42801  fprodexp  42810  mccl  42814  fprodcnlem  42815  fprodcn  42816  climmulf  42820  climexp  42821  climsuse  42824  climrecf  42825  climinff  42827  climaddf  42831  mullimc  42832  islptre  42835  climf  42838  mullimcf  42839  rexlim2d  42841  idlimc  42842  limcperiod  42844  limcrecl  42845  islpcn  42855  limsupre  42857  limcleqr  42860  addlimc  42864  limclner  42867  climsubmpt  42876  climreclf  42880  climf2  42882  climeldmeqmpt  42884  clim2f2  42886  climfveqmpt  42887  fnlimfvre  42890  allbutfifvre  42891  climleltrp  42892  fnlimf  42894  fnlimabslt  42895  climfveqf  42896  climfveqmpt3  42898  climeldmeqf  42899  climeqf  42904  climeldmeqmpt3  42905  limsuppnfd  42918  limsupub  42920  climinf2lem  42922  climinf2  42923  limsuppnf  42927  limsupubuz  42929  climinf2mpt  42930  climinfmpt  42931  climinf3  42932  limsupmnflem  42936  limsupequz  42939  limsupre2  42941  limsupmnfuzlem  42942  limsupequzmptf  42947  limsupre3  42949  limsupre3uzlem  42951  limsupreuzmpt  42955  climisp  42962  lmbr3  42963  climrescn  42964  climxrrelem  42965  climxrre  42966  limsupub2  43028  liminflbuz2  43031  xlimmnfvlem2  43049  xlimmnfv  43050  xlimpnfvlem2  43053  xlimpnfv  43054  xlimmnfmpt  43059  xlimpnfmpt  43060  climxlim2lem  43061  cncficcgt0  43104  cncfioobd  43113  fprodsubrecnncnvlem  43123  fprodaddrecnncnvlem  43125  dvmptmulf  43153  dvnmul  43159  dvmptfprodlem  43160  dvmptfprod  43161  dvnprodlem1  43162  dvnprodlem2  43163  iblsplitf  43186  itgperiod  43197  stoweidlem3  43219  stoweidlem26  43242  stoweidlem27  43243  stoweidlem29  43245  stoweidlem31  43247  stoweidlem34  43250  stoweidlem35  43251  stoweidlem36  43252  stoweidlem39  43255  stoweidlem42  43258  stoweidlem43  43259  stoweidlem44  43260  stoweidlem46  43262  stoweidlem48  43264  stoweidlem49  43265  stoweidlem51  43267  stoweidlem52  43268  stoweidlem53  43269  stoweidlem54  43270  stoweidlem55  43271  stoweidlem56  43272  stoweidlem57  43273  stoweidlem58  43274  stoweidlem59  43275  stoweidlem60  43276  stoweidlem61  43277  stoweidlem62  43278  stoweid  43279  wallispilem3  43283  stirlinglem13  43302  stirling  43305  fourierdlem16  43339  fourierdlem21  43344  fourierdlem22  43345  fourierdlem31  43354  fourierdlem39  43362  fourierdlem48  43370  fourierdlem51  43373  fourierdlem68  43390  fourierdlem71  43393  fourierdlem73  43395  fourierdlem80  43402  fourierdlem81  43403  fourierdlem86  43408  fourierdlem87  43409  fourierdlem93  43415  fourierdlem94  43416  fourierdlem103  43425  fourierdlem104  43426  fourierdlem112  43434  fourierdlem113  43435  elaa2  43450  etransclem32  43482  salexct  43548  sge0revalmpt  43591  sge0f1o  43595  sge0lefi  43611  sge0resplit  43619  sge0lempt  43623  sge0iunmptlemre  43628  sge0fodjrnlem  43629  sge0iunmpt  43631  sge0ltfirpmpt2  43639  sge0isum  43640  sge0xp  43642  sge0isummpt2  43645  sge0xadd  43648  sge0pnffsumgt  43655  sge0gtfsumgt  43656  sge0uzfsumgt  43657  sge0reuz  43660  sge0reuzb  43661  iundjiun  43673  meadjiun  43679  ismeannd  43680  voliunsge0lem  43685  meaiunincf  43696  meaiuninc3v  43697  meaiuninc3  43698  meaiininc  43700  caragenfiiuncl  43728  omeiunltfirp  43732  ovnsubaddlem2  43784  hoidmvval0  43800  hoidmvlelem1  43808  hoidmvlelem3  43810  hoidmvlelem5  43812  ovnlecvr2  43823  hspdifhsp  43829  hoiqssbllem2  43836  hoiqssbllem3  43837  hspmbllem2  43840  opnvonmbllem2  43846  hoimbl2  43878  vonhoire  43885  iinhoiicc  43887  iunhoiioolem  43888  iunhoiioo  43889  vonioo  43895  vonicc  43898  vonn0ioo2  43903  vonn0icc2  43905  salpreimagelt  43917  salpreimalegt  43919  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  preimageiingt  43929  preimaleiinlt  43930  salpreimagtge  43933  salpreimaltle  43934  salpreimalelt  43937  salpreimagtlt  43938  incsmflem  43949  issmflelem  43952  issmfle  43953  smfconst  43957  issmfgtlem  43963  issmfgt  43964  smfaddlem2  43971  smfadd  43972  decsmflem  43973  decsmf  43974  issmfgelem  43976  issmfge  43977  smflimlem2  43979  smflim  43984  smfresal  43994  smfrec  43995  smfmullem4  44000  smfmul  44001  smfpimcc  44013  smflimmpt  44015  smfsuplem1  44016  smfsupmpt  44020  smfsupxr  44021  smfinflem  44022  smfinfmpt  44024  smflimsuplem5  44029  smflimsuplem7  44031  smflimsuplem8  44032  smflimsupmpt  44034  smfliminflem  44035  smfliminfmpt  44037  or2expropbilem2  44199  or2expropbi  44200  cfsetsnfsetf  44224  2reu8i  44277  nfdfat  44291  iccelpart  44558  ichnfim  44589  ich2exprop  44596  ichreuopeq  44598  sprsymrelfo  44622  reupr  44647  reuopreuprim  44651  2zrngmmgm  45177  opeliun2xp  45341  cbvmpox2  45344  ovmpordxf  45347  1arymaptfo  45662  2arymaptfo  45673  setrec1  46068  aacllem  46176