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 395  ⊤wtru 1540  Ⅎwnf 1787

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfnan  1904  nf3an  1905  hban  2300  nfeqf  2381  nfald2  2445  2ax6elem  2470  nfsb4t  2503  nfeu1ALT  2589  eupicka  2636  mopick2  2639  2mo  2650  clelabOLD  2883  nfabd2  2932  2ralbida  3159  r19.12  3252  r19.12OLD  3253  ralcom2  3288  reean  3291  cbvreuw  3365  cbvrmow  3366  cbvreu  3370  cbvrabw  3414  cbvrab  3415  ralimda  3421  ceqsex2  3472  vtocl2gaf  3505  spc2ed  3530  rspce  3540  eqvincf  3572  elrabf  3613  elrab3t  3616  rexab2  3630  rexab2OLD  3631  morex  3649  reu2  3655  rmo3f  3664  reu2eqd  3666  sbc2iegf  3794  reu8nf  3806  rmo2  3816  rmo3  3818  csbiebt  3858  csbie2t  3869  cbvrabcsfw  3872  cbvreucsf  3875  cbvrabcsf  3876  reusngf  4605  rexreusng  4612  reuprg0  4635  rabsnifsb  4655  nfop  4817  nfopd  4818  eluniab  4851  iuneqconst  4932  cbvopab  5142  cbvopab1  5145  cbvopab1g  5146  cbvopab2  5147  cbvopab1s  5148  mpteq12f  5158  nfmpt  5177  cbvmptf  5179  cbvmptfg  5180  axrep3  5209  axrep4  5210  axrep5  5211  reusv2lem3  5318  axprlem4  5344  axprlem5  5345  nfpo  5499  nfso  5500  nffr  5554  nfwe  5556  nfxp  5613  opeliunxp  5645  nfco  5763  elrnmpt1  5856  nfimad  5967  reuop  6185  iota2  6407  nffun  6441  imadif  6502  nffn  6516  nff  6580  nff1  6652  nffo  6671  nff1o  6698  nffvd  6768  fv3  6774  fvmptdf  6863  f1ossf1o  6982  fmptco  6983  fsnex  7135  nfiso  7173  nfriotadw  7220  cbvriotaw  7221  nfriotad  7224  cbvriota  7226  riota2df  7236  riota5f  7241  oprabv  7313  nfoprab  7317  mpoeq123  7325  nfmpo  7335  cbvoprab1  7340  cbvoprab2  7341  cbvoprab12  7342  cbvoprab3  7344  cbvmpox  7346  ovmpodxf  7401  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  onminex  7629  peano5OLD  7715  fiun  7759  f1iun  7760  opabex3d  7781  opabex3rd  7782  opabex3  7783  dfoprab4f  7869  fmpox  7880  opeliunxp2f  7997  nffrecs  8070  frrlem4  8076  nfwrecsOLD  8104  wfrlem4OLD  8114  tfr3  8201  tz7.49  8246  erovlem  8560  nfixpw  8662  nfixp  8663  nfixp1  8664  xpf1o  8875  nneneq  8896  ac6sfi  8988  nfoi  9203  wdom2d  9269  trpredmintr  9409  infpssrlem4  9993  hsmexlem2  10114  hsmexlem4  10116  domtriomlem  10129  axdc3lem2  10138  axdc4lem  10142  zorn2lem4  10186  zorn2lem5  10187  konigthlem  10255  axextnd  10278  axrepndlem2  10280  axrepnd  10281  axunnd  10283  axpowndlem2  10285  axpowndlem4  10287  axpownd  10288  axregndlem2  10290  axregnd  10291  axinfndlem1  10292  axinfnd  10293  zfcndrep  10301  zfcndinf  10305  dedekind  11068  dedekindle  11069  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  fsuppmapnn0fiubex  13640  reuccatpfxs1  14388  nfsum1  15329  nfsum  15330  nfsumOLD  15331  fsumclf  15378  fsumsplitf  15382  fsumsplit1  15385  fsum2dlem  15410  fsum00  15438  nfcprod1  15548  nfcprod  15549  fprod2dlem  15618  fprodsplitf  15626  fprodsplit1f  15628  fprodle  15634  lcmfunsnlem1  16270  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  mreexexd  17274  acsmapd  18187  gsum2d2lem  19489  dprd2d2  19562  gsummoncoe1  21385  gsummatr01lem4  21715  cpmatmcllem  21775  cayleyhamilton1  21949  neiptopnei  22191  neiptopreu  22192  neitr  22239  iunconnlem  22486  iunconn  22487  ptcnplem  22680  ptcnp  22681  xkocnv  22873  isfildlem  22916  utopsnneiplem  23307  isucn2  23339  cfilucfil  23621  restmetu  23632  ovolfiniun  24570  ovoliunlem3  24573  ovoliunnul  24576  volfiniun  24616  itg2splitlem  24818  itg2split  24819  isibl2  24836  nfitg  24844  cbvitg  24845  limciun  24963  2sqmo  26490  2sqreulem4  26507  istrkg2ld  26725  chirred  30658  sbc2iedf  30716  rspc2daf  30717  opreu2reuALT  30726  mo5f  30738  foresf1o  30751  iinabrex  30809  cbvdisjf  30811  disjabrex  30822  disjabrexf  30823  funimass4f  30873  2ndresdju  30887  fmptcof2  30896  fcomptf  30897  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1lem  30901  funcnv4mpt  30908  fnpreimac  30910  cnvoprabOLD  30957  f1od2  30958  fpwrelmap  30970  xrofsup  30992  nn0min  31036  fprodex01  31041  fsumiunle  31045  isarchiofld  31418  nsgqusf1olem1  31500  nsgqusf1olem3  31502  elrspunidl  31508  fedgmullem2  31613  reff  31691  locfinreflem  31692  cmpcref  31702  zarclsiin  31723  zarcmplem  31733  ordtconnlem1  31776  prodindf  31891  esumcl  31898  gsumesum  31927  esumlub  31928  esumcst  31931  esumrnmpt2  31936  esumfzf  31937  esumfsup  31938  hasheuni  31953  esumcvg  31954  esumgect  31958  esumcvgre  31959  esum2dlem  31960  esum2d  31961  esumiun  31962  ldsysgenld  32028  sigapildsyslem  32029  sigapildsys  32030  ldgenpisyslem1  32031  measvunilem  32080  measvunilem0  32081  measvuni  32082  measinblem  32088  voliune  32097  volfiniune  32098  volmeas  32099  oms0  32164  omssubadd  32167  eulerpartlemgvv  32243  dstrvprob  32338  breprexplema  32510  bnj919  32647  bnj1146  32671  bnj1379  32710  bnj849  32805  bnj916  32813  bnj964  32823  bnj1014  32841  bnj1123  32866  bnj1228  32891  bnj1307  32903  bnj1321  32907  bnj1398  32914  bnj1408  32916  bnj1444  32923  bnj1445  32924  bnj1446  32925  bnj1449  32928  bnj1467  32934  bnj1463  32935  bnj1489  32936  bnj1491  32937  bnj1312  32938  bnj1525  32949  fineqvrep  32964  cvmcov  33125  iota5f  33571  axextdist  33681  axextbdist  33682  nfwlim  33743  finminlem  34434  bj-dvelimdv  34962  bj-opabco  35286  isbasisrelowllem1  35453  isbasisrelowllem2  35454  fvineqsneu  35509  fvineqsneq  35510  wl-cbvalnaed  35618  wl-2sb6d  35640  wl-sbalnae  35644  wl-mo2tf  35653  wl-eutf  35655  wl-ax11-lem3  35665  phpreu  35688  poimirlem26  35730  poimirlem27  35731  heicant  35739  mbfposadd  35751  ftc1anclem5  35781  indexdom  35819  filbcmb  35825  sdclem2  35827  sdclem1  35828  fdc1  35831  riotasv2d  36898  riotasv2s  36899  nfded2  36909  glbconxN  37319  pmapglb2xN  37713  cdlemefs32sn1aw  38355  mzpsubmpt  40481  mzpexpmpt  40483  eq0rabdioph  40514  eqrabdioph  40515  setindtr  40762  ss2iundf  41156  scottabf  41747  mnuprdlem4  41782  ismnushort  41808  binomcxplemnotnn0  41863  iunconnlem2  42444  elunif  42448  rspcegf  42455  fnchoice  42461  refsumcn  42462  rfcnnnub  42468  uzwo4  42490  fiiuncl  42502  cbvmpo2  42536  cbvmpo1  42537  iinssiin  42567  disjf1  42609  disjrnmpt2  42615  disjf1o  42618  fompt  42619  disjinfi  42620  choicefi  42629  axccdom  42651  dmrelrnrel  42654  axccd  42657  funimassd  42659  rnmptbddlem  42678  rnmptbd2lem  42683  infnsuprnmpt  42685  rnmptbdlem  42690  rnmptssbi  42696  upbdrech  42734  ssfiunibd  42738  supxrgere  42762  supxrgelem  42766  supxrge  42767  xralrple2  42783  infxr  42796  infxrunb2  42797  xrralrecnnle  42812  xrralrecnnge  42820  supxrunb3  42829  supxrleubrnmpt  42836  infleinf2  42844  unb2ltle  42845  rexabslelem  42848  suprleubrnmpt  42852  uzub  42861  supminfrnmpt  42875  supxrleubrnmptf  42881  infxrgelbrnmpt  42884  infrpgernmpt  42895  monoordxr  42913  monoord2xr  42915  iccshift  42946  iooshift  42950  iooiinicc  42970  iooiinioc  42984  fsummulc1f  43002  fsumf1of  43005  fsumreclf  43007  fsumlessf  43008  fmul01  43011  fmuldfeqlem1  43013  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  fprodexp  43025  mccl  43029  fprodcnlem  43030  fprodcn  43031  climmulf  43035  climexp  43036  climsuse  43039  climrecf  43040  climinff  43042  climaddf  43046  mullimc  43047  islptre  43050  climf  43053  mullimcf  43054  rexlim2d  43056  idlimc  43057  limcperiod  43059  limcrecl  43060  islpcn  43070  limsupre  43072  limcleqr  43075  addlimc  43079  limclner  43082  climsubmpt  43091  climreclf  43095  climf2  43097  climeldmeqmpt  43099  clim2f2  43101  climfveqmpt  43102  fnlimfvre  43105  allbutfifvre  43106  climleltrp  43107  fnlimf  43109  fnlimabslt  43110  climfveqf  43111  climfveqmpt3  43113  climeldmeqf  43114  climeqf  43119  climeldmeqmpt3  43120  limsuppnfd  43133  limsupub  43135  climinf2lem  43137  climinf2  43138  limsuppnf  43142  limsupubuz  43144  climinf2mpt  43145  climinfmpt  43146  climinf3  43147  limsupmnflem  43151  limsupequz  43154  limsupre2  43156  limsupmnfuzlem  43157  limsupequzmptf  43162  limsupre3  43164  limsupre3uzlem  43166  limsupreuzmpt  43170  climisp  43177  lmbr3  43178  climrescn  43179  climxrrelem  43180  climxrre  43181  limsupub2  43243  liminflbuz2  43246  xlimmnfvlem2  43264  xlimmnfv  43265  xlimpnfvlem2  43268  xlimpnfv  43269  xlimmnfmpt  43274  xlimpnfmpt  43275  climxlim2lem  43276  cncficcgt0  43319  cncfioobd  43328  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  dvmptmulf  43368  dvnmul  43374  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem2  43378  iblsplitf  43401  itgperiod  43412  stoweidlem3  43434  stoweidlem26  43457  stoweidlem27  43458  stoweidlem29  43460  stoweidlem31  43462  stoweidlem34  43465  stoweidlem35  43466  stoweidlem36  43467  stoweidlem39  43470  stoweidlem42  43473  stoweidlem43  43474  stoweidlem44  43475  stoweidlem46  43477  stoweidlem48  43479  stoweidlem49  43480  stoweidlem51  43482  stoweidlem52  43483  stoweidlem53  43484  stoweidlem54  43485  stoweidlem55  43486  stoweidlem56  43487  stoweidlem57  43488  stoweidlem58  43489  stoweidlem59  43490  stoweidlem60  43491  stoweidlem61  43492  stoweidlem62  43493  stoweid  43494  wallispilem3  43498  stirlinglem13  43517  stirling  43520  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem31  43569  fourierdlem39  43577  fourierdlem48  43585  fourierdlem51  43588  fourierdlem68  43605  fourierdlem71  43608  fourierdlem73  43610  fourierdlem80  43617  fourierdlem81  43618  fourierdlem86  43623  fourierdlem87  43624  fourierdlem93  43630  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  elaa2  43665  etransclem32  43697  salexct  43763  sge0revalmpt  43806  sge0f1o  43810  sge0lefi  43826  sge0resplit  43834  sge0lempt  43838  sge0iunmptlemre  43843  sge0fodjrnlem  43844  sge0iunmpt  43846  sge0ltfirpmpt2  43854  sge0isum  43855  sge0xp  43857  sge0isummpt2  43860  sge0xadd  43863  sge0pnffsumgt  43870  sge0gtfsumgt  43871  sge0uzfsumgt  43872  sge0reuz  43875  sge0reuzb  43876  iundjiun  43888  meadjiun  43894  ismeannd  43895  voliunsge0lem  43900  meaiunincf  43911  meaiuninc3v  43912  meaiuninc3  43913  meaiininc  43915  caragenfiiuncl  43943  omeiunltfirp  43947  ovnsubaddlem2  43999  hoidmvval0  44015  hoidmvlelem1  44023  hoidmvlelem3  44025  hoidmvlelem5  44027  ovnlecvr2  44038  hspdifhsp  44044  hoiqssbllem2  44051  hoiqssbllem3  44052  hspmbllem2  44055  opnvonmbllem2  44061  hoimbl2  44093  vonhoire  44100  iinhoiicc  44102  iunhoiioolem  44103  iunhoiioo  44104  vonioo  44110  vonicc  44113  vonn0ioo2  44118  vonn0icc2  44120  salpreimagelt  44132  salpreimalegt  44134  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  preimageiingt  44144  preimaleiinlt  44145  salpreimagtge  44148  salpreimaltle  44149  salpreimalelt  44152  salpreimagtlt  44153  incsmflem  44164  issmflelem  44167  issmfle  44168  smfconst  44172  issmfgtlem  44178  issmfgt  44179  smfaddlem2  44186  smfadd  44187  decsmflem  44188  decsmf  44189  issmfgelem  44191  issmfge  44192  smflimlem2  44194  smflim  44199  smfresal  44209  smfrec  44210  smfmullem4  44215  smfmul  44216  smfpimcc  44228  smflimmpt  44230  smfsuplem1  44231  smfsupmpt  44235  smfsupxr  44236  smfinflem  44237  smfinfmpt  44239  smflimsuplem5  44244  smflimsuplem7  44246  smflimsuplem8  44247  smflimsupmpt  44249  smfliminflem  44250  smfliminfmpt  44252  or2expropbilem2  44414  or2expropbi  44415  cfsetsnfsetf  44439  2reu8i  44492  nfdfat  44506  iccelpart  44773  ichnfim  44804  ich2exprop  44811  ichreuopeq  44813  sprsymrelfo  44837  reupr  44862  reuopreuprim  44866  2zrngmmgm  45392  opeliun2xp  45556  cbvmpox2  45559  ovmpordxf  45562  1arymaptfo  45877  2arymaptfo  45888  setrec1  46283  aacllem  46391