Theorem nfan 1828

Description: If x is not free in ph and ps, it is not free in ( ph /\ ps ). (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	|- F/ x ph
nfan.2	|- F/ x ps

Assertion

Ref	Expression
nfan	|- F/ x ( ph /\ ps )

Proof of Theorem nfan

Step	Hyp	Ref	Expression
1		nfan.1	. . . 4 |- F/ x ph
2	1	a1i 11	. . 3 |- ( T. -> F/ x ph )
3		nfan.2	. . . 4 |- F/ x ps
4	3	a1i 11	. . 3 |- ( T. -> F/ x ps )
5	2, 4	nfand 1826	. 2 |- ( T. -> F/ x ( ph /\ ps ) )
6	5	trud 1493	1 |- F/ x ( ph /\ ps )

Syntax hints:   /\ wa 384   T. wtru 1484   F/wnf 1708

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfnan  1830  nf3an  1831  hban  2128  nfeqf  2301  nfald2  2331  nfsb4t  2389  2ax6elem  2449  eupicka  2537  mopick2  2540  2mo  2551  axbnd  2601  clelab  2748  nfabd2  2784  2ralbida  2987  r19.29an  3077  ralcom2  3104  reean  3106  cbvreu  3169  cbvrab  3198  ceqsex2  3244  vtocl2gaf  3273  rspce  3304  eqvincf  3331  elrabf  3360  elrab3t  3362  rexab2  3373  morex  3390  reu2  3394  reu2eqd  3403  sbc2iegf  3504  reu8nf  3516  rmo2  3526  rmo3  3528  csbiebt  3553  csbie2t  3562  cbvreucsf  3567  cbvrabcsf  3568  rabsnifsb  4257  nfop  4418  nfopd  4419  eluniab  4447  dfnfc2OLD  4455  nfopab  4718  cbvopab  4721  cbvopab1  4723  cbvopab2  4724  cbvopab1s  4725  mpteq12f  4731  nfmpt  4746  cbvmptf  4748  cbvmpt  4749  axrep3  4774  axrep4  4775  axrep5  4776  reusv2lem2OLD  4870  reusv2lem3  4871  nfpo  5040  nfso  5041  nffr  5088  nfwe  5090  nfxp  5142  opeliunxp  5170  nfco  5287  elrnmpt1  5374  nfimad  5475  elsnxpOLD  5678  iota2  5877  nffun  5911  imadif  5973  nffn  5987  nff  6041  nff1  6099  nffo  6114  nff1o  6135  nffvd  6200  fv3  6206  fmptco  6396  fsnex  6538  nfiso  6572  nfriotad  6619  cbvriota  6621  riota2df  6631  riota5f  6636  oprabv  6703  nfoprab  6707  mpt2eq123  6714  nfmpt2  6724  cbvoprab1  6727  cbvoprab2  6728  cbvoprab12  6729  cbvoprab3  6731  cbvmpt2x  6733  ovmpt2dxf  6786  elovmpt2rab  6880  elovmpt2rab1  6881  onminex  7007  peano5  7089  fun11iun  7126  opabex3d  7145  opabex3  7146  dfoprab4f  7226  fmpt2x  7236  opeliunxp2f  7336  nfwrecs  7409  wfrlem4  7418  tfr3  7495  tz7.49  7540  erovlem  7843  nfixp  7927  nfixp1  7928  xpf1o  8122  nneneq  8143  ac6sfi  8204  nfoi  8419  wdom2d  8485  infpssrlem4  9128  hsmexlem2  9249  hsmexlem4  9251  domtriomlem  9264  axdc3lem2  9273  axdc4lem  9277  zorn2lem4  9321  zorn2lem5  9322  konigthlem  9390  axextnd  9413  axrepndlem2  9415  axrepnd  9416  axunnd  9418  axpowndlem2  9420  axpowndlem4  9422  axpownd  9423  axregndlem2  9425  axregnd  9426  axinfndlem1  9427  axinfnd  9428  zfcndrep  9436  zfcndinf  9440  dedekind  10200  dedekindle  10201  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  fsuppmapnn0fiubex  12792  reuccats1  13480  nfsum1  14420  nfsum  14421  fsumsplitf  14472  fsum2dlem  14501  fsum00  14530  nfcprod1  14640  nfcprod  14641  fprod2dlem  14710  fprodsplitf  14719  fprodsplit1f  14721  fprodle  14727  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  mreexexd  16308  mreexexdOLD  16309  acsmapd  17178  gsum2d2lem  18372  dprd2d2  18443  gsummoncoe1  19674  gsummatr01lem4  20464  cpmatmcllem  20523  pmatcollpwfi  20587  cayleyhamilton1  20697  neiptopnei  20936  neiptopreu  20937  neitr  20984  iunconnlem  21230  iunconn  21231  ptcnplem  21424  ptcnp  21425  xkocnv  21617  isfildlem  21661  utopsnneiplem  22051  isucn2  22083  cfilucfil  22364  restmetu  22375  ovolfiniun  23269  ovoliunlem3  23272  ovoliunnul  23275  volfiniun  23315  itg2splitlem  23515  itg2split  23516  isibl2  23533  nfitg  23541  cbvitg  23542  limciun  23658  istrkg2ld  25359  chirred  29254  spc2ed  29312  mo5f  29324  rmo3f  29335  rmo4fOLD  29336  foresf1o  29343  cbvdisjf  29385  disjabrex  29395  disjabrexf  29396  funimass4f  29437  fmptcof2  29457  fcomptf  29458  acunirnmpt2  29460  acunirnmpt2f  29461  aciunf1lem  29462  funcnv4mpt  29470  cnvoprab  29498  f1od2  29499  fpwrelmap  29508  xrofsup  29533  nn0min  29567  fprodex01  29571  fsumiunle  29575  2sqmo  29649  isarchiofld  29817  reff  29906  locfinreflem  29907  cmpcref  29917  ordtconnlem1  29970  prodindf  30085  esumcl  30092  gsumesum  30121  esumlub  30122  esumcst  30125  esumrnmpt2  30130  esumfzf  30131  esumfsup  30132  hasheuni  30147  esumcvg  30148  esumgect  30152  esumcvgre  30153  esum2dlem  30154  esum2d  30155  esumiun  30156  ldsysgenld  30223  sigapildsyslem  30224  sigapildsys  30225  ldgenpisyslem1  30226  measvunilem  30275  measvunilem0  30276  measvuni  30277  measinblem  30283  voliune  30292  volfiniune  30293  volmeas  30294  oms0  30359  omssubadd  30362  eulerpartlemgvv  30438  dstrvprob  30533  breprexplema  30708  bnj919  30837  bnj1146  30862  bnj1379  30901  bnj849  30995  bnj916  31003  bnj964  31013  bnj1014  31030  bnj1123  31054  bnj1228  31079  bnj1307  31091  bnj1321  31095  bnj1398  31102  bnj1408  31104  bnj1444  31111  bnj1445  31112  bnj1446  31113  bnj1449  31116  bnj1467  31122  bnj1463  31123  bnj1489  31124  bnj1491  31125  bnj1312  31126  bnj1525  31137  cvmcov  31245  iota5f  31606  axextdist  31705  axext4dist  31706  trpredmintr  31731  nfwlim  31768  frrlem4  31783  finminlem  32312  bj-axrep3  32790  bj-axrep4  32791  bj-axrep5  32792  bj-dvelimdv  32834  isbasisrelowllem1  33203  isbasisrelowllem2  33204  wl-cbvalnaed  33319  wl-2sb6d  33341  wl-sbalnae  33345  wl-mo2tf  33353  wl-eutf  33355  wl-ax11-lem3  33364  phpreu  33393  poimirlem26  33435  poimirlem27  33436  heicant  33444  mbfposadd  33457  ftc1anclem5  33489  indexdom  33529  filbcmb  33535  sdclem2  33538  sdclem1  33539  fdc1  33542  riotasv2d  34243  riotasv2s  34244  nfded2  34255  glbconxN  34664  pmapglb2xN  35058  cdlemefs32sn1aw  35702  mzpsubmpt  37306  mzpexpmpt  37308  eq0rabdioph  37340  eqrabdioph  37341  setindtr  37591  ss2iundf  37951  binomcxplemnotnn0  38555  iunconnlem2  39171  elunif  39175  rspcegf  39182  fnchoice  39188  refsumcn  39189  rfcnnnub  39195  uzwo4  39221  fiiuncl  39234  cbvmpt22  39277  cbvmpt21  39278  iinssiin  39312  ralimda  39326  disjf1  39369  wessf1ornlem  39371  disjrnmpt2  39375  disjf1o  39378  fompt  39379  disjinfi  39380  choicefi  39392  axccdom  39416  dmrelrnrel  39419  axccd  39429  funimassd  39431  rnmptbddlem  39455  rnmptbd2lem  39463  infnsuprnmpt  39465  rnmptbdlem  39470  rnmptssbi  39477  upbdrech  39519  ssfiunibd  39523  supxrgere  39549  supxrgelem  39553  supxrge  39554  xralrple2  39570  infxr  39583  infxrunb2  39584  xrralrecnnle  39602  xrralrecnnge  39613  supxrunb3  39623  supxrleubrnmpt  39632  infleinf2  39641  unb2ltle  39642  rexabslelem  39645  suprleubrnmpt  39649  uzub  39658  supminfrnmpt  39672  supxrleubrnmptf  39680  infxrgelbrnmpt  39683  infrpgernmpt  39695  iccshift  39744  iooshift  39748  iooiinicc  39769  iooiinioc  39783  fsumclf  39801  fsummulc1f  39802  fsumsplit1  39804  fsumf1of  39806  fsumreclf  39808  fsumlessf  39809  fmul01  39812  fmuldfeqlem1  39814  fmuldfeq  39815  fmul01lt1lem1  39816  fmul01lt1lem2  39817  fprodexp  39826  mccl  39830  fprodcnlem  39831  fprodcn  39832  climmulf  39836  climexp  39837  climsuse  39840  climrecf  39841  climinff  39843  climaddf  39847  mullimc  39848  islptre  39851  climf  39854  mullimcf  39855  rexlim2d  39857  idlimc  39858  limcperiod  39860  limcrecl  39861  islpcn  39871  limsupre  39873  limcleqr  39876  addlimc  39880  limclner  39883  climsubmpt  39892  climreclf  39896  climf2  39898  climeldmeqmpt  39900  clim2f2  39902  climfveqmpt  39903  fnlimfvre  39906  allbutfifvre  39907  climleltrp  39908  fnlimf  39910  fnlimabslt  39911  climfveqf  39912  climfveqmpt3  39914  climeldmeqf  39915  climeqf  39920  climeldmeqmpt3  39921  limsuppnfd  39934  limsupub  39936  climinf2lem  39938  climinf2  39939  limsuppnf  39943  limsupubuz  39945  climinf2mpt  39946  climinfmpt  39947  climinf3  39948  limsupmnflem  39952  limsupequz  39955  limsupre2  39957  limsupmnfuzlem  39958  limsupequzmptf  39963  limsupre3  39965  limsupre3uzlem  39967  limsupreuzmpt  39971  climisp  39978  lmbr3  39979  climrescn  39980  climxrrelem  39981  climxrre  39982  xlimmnfvlem2  40059  xlimmnfv  40060  xlimpnfvlem2  40063  xlimpnfv  40064  xlimmnfmpt  40069  xlimpnfmpt  40070  climxlim2lem  40071  cncficcgt0  40101  cncfioobd  40110  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  dvmptmulf  40152  dvnmul  40158  dvmptfprodlem  40159  dvmptfprod  40160  dvnprodlem1  40161  dvnprodlem2  40162  iblsplitf  40186  itgperiod  40197  stoweidlem3  40220  stoweidlem26  40243  stoweidlem27  40244  stoweidlem29  40246  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem36  40253  stoweidlem39  40256  stoweidlem42  40259  stoweidlem43  40260  stoweidlem44  40261  stoweidlem46  40263  stoweidlem48  40265  stoweidlem49  40266  stoweidlem51  40268  stoweidlem52  40269  stoweidlem53  40270  stoweidlem54  40271  stoweidlem55  40272  stoweidlem56  40273  stoweidlem57  40274  stoweidlem58  40275  stoweidlem59  40276  stoweidlem60  40277  stoweidlem61  40278  stoweidlem62  40279  stoweid  40280  wallispilem3  40284  stirlinglem13  40303  stirling  40306  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem31  40355  fourierdlem39  40363  fourierdlem48  40371  fourierdlem51  40374  fourierdlem53  40376  fourierdlem68  40391  fourierdlem71  40394  fourierdlem73  40396  fourierdlem80  40403  fourierdlem81  40404  fourierdlem86  40409  fourierdlem87  40410  fourierdlem93  40416  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  elaa2  40451  etransclem32  40483  salexct  40552  sge0revalmpt  40595  sge0f1o  40599  sge0lefi  40615  sge0resplit  40623  sge0lempt  40627  sge0iunmptlemre  40632  sge0fodjrnlem  40633  sge0iunmpt  40635  sge0ltfirpmpt2  40643  sge0isum  40644  sge0xp  40646  sge0isummpt2  40649  sge0xadd  40652  sge0pnffsumgt  40659  sge0gtfsumgt  40660  sge0uzfsumgt  40661  sge0reuz  40664  sge0reuzb  40665  iundjiun  40677  meadjiun  40683  ismeannd  40684  voliunsge0lem  40689  meaiininc  40701  caragenfiiuncl  40729  omeiunltfirp  40733  ovnsubaddlem2  40785  hoidmvval0  40801  hoidmvlelem1  40809  hoidmvlelem3  40811  hoidmvlelem5  40813  ovnlecvr2  40824  hspdifhsp  40830  hoiqssbllem2  40837  hoiqssbllem3  40838  hspmbllem2  40841  opnvonmbllem2  40847  hoimbl2  40879  vonhoire  40886  iinhoiicc  40888  iunhoiioolem  40889  iunhoiioo  40890  vonioo  40896  vonicc  40899  vonn0ioo2  40904  vonn0icc2  40906  salpreimagelt  40918  salpreimalegt  40920  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  preimageiingt  40930  preimaleiinlt  40931  salpreimagtge  40934  salpreimaltle  40935  salpreimalelt  40938  salpreimagtlt  40939  incsmflem  40950  issmflelem  40953  issmfle  40954  smfconst  40958  issmfgtlem  40964  issmfgt  40965  smfaddlem2  40972  smfadd  40973  decsmflem  40974  decsmf  40975  issmfgelem  40977  issmfge  40978  smflimlem2  40980  smflim  40985  smfresal  40995  smfrec  40996  smfmullem4  41001  smfmul  41002  smfpimcc  41014  smflimmpt  41016  smfsuplem1  41017  smfsupmpt  41021  smfsupxr  41022  smfinflem  41023  smfinfmpt  41025  smflimsuplem5  41030  smflimsuplem7  41032  smflimsuplem8  41033  smflimsupmpt  41035  smfliminflem  41036  smfliminfmpt  41038  nfdfat  41210  iccelpart  41369  sprsymrelfo  41747  2zrngmmgm  41946  opeliun2xp  42111  cbvmpt2x2  42114  ovmpt2rdxf  42117  setrec1  42438  aacllem  42547