MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfan Structured version   Visualization version   GIF version

Theorem nfan 1816
Description: If 𝑥 is not free in 𝜑 and 𝜓, 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
StepHypRef Expression
1 nfan.1 . . . 4 𝑥𝜑
21a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
3 nfan.2 . . . 4 𝑥𝜓
43a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜓)
52, 4nfand 1814 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65trud 1484 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wa 383  wtru 1476  wnf 1699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701
This theorem is referenced by:  nfnan  1818  nf3an  1819  hban  2113  nfeqf  2289  nfald2  2319  nfsb4t  2377  2ax6elem  2437  eupicka  2525  mopick2  2528  2mo  2539  axbnd  2589  clelab  2735  nfabd2  2770  2ralbida  2970  r19.29an  3059  ralcom2  3083  reean  3085  cbvreu  3145  cbvrab  3171  ceqsex2  3217  vtocl2gaf  3246  rspce  3277  eqvincf  3301  elrabf  3329  elrab3t  3330  rexab2  3340  morex  3357  reu2  3361  reu2eqd  3370  sbc2iegf  3471  rmo2  3492  rmo3  3494  csbiebt  3519  csbie2t  3528  cbvreucsf  3533  cbvrabcsf  3534  rabsnifsb  4201  nfop  4356  nfopd  4357  eluniab  4383  dfnfc2OLD  4391  rabasiun  4459  nfopab  4650  cbvopab  4653  cbvopab1  4655  cbvopab2  4656  cbvopab1s  4657  mpteq12f  4661  nfmpt  4674  cbvmptf  4676  cbvmpt  4677  axrep3  4702  axrep4  4703  axrep5  4704  reusv2lem2OLD  4796  reusv2lem3  4797  nfpo  4964  nfso  4965  nffr  5012  nfwe  5014  nfxp  5066  opeliunxp  5093  nfco  5209  elrnmpt1  5295  nfimad  5394  elsnxpOLD  5595  iota2  5794  nffun  5826  imadif  5887  nffn  5901  nff  5954  nff1  6012  nffo  6027  nff1o  6048  nffvd  6112  fv3  6116  fmptco  6303  fsnex  6438  nfiso  6472  nfriotad  6519  cbvriota  6521  riota2df  6531  riota5f  6535  oprabv  6601  nfoprab  6605  mpt2eq123  6612  nfmpt2  6622  cbvoprab1  6625  cbvoprab2  6626  cbvoprab12  6627  cbvoprab3  6629  cbvmpt2x  6631  ovmpt2dxf  6684  elovmpt2rab  6778  elovmpt2rab1  6779  onminex  6899  peano5  6981  fun11iun  7019  opabex3d  7037  opabex3  7038  dfoprab4f  7117  fmpt2x  7125  opeliunxp2f  7223  nfwrecs  7296  wfrlem4  7305  tfr3  7382  tz7.49  7427  erovlem  7730  nfixp  7813  nfixp1  7814  xpf1o  8007  nneneq  8028  ac6sfi  8089  nfoi  8302  wdom2d  8368  infpssrlem4  9011  hsmexlem2  9132  hsmexlem4  9134  domtriomlem  9147  axdc3lem2  9156  axdc4lem  9160  zorn2lem4  9204  zorn2lem5  9205  konigthlem  9269  axextnd  9292  axrepndlem2  9294  axrepnd  9295  axunnd  9297  axpowndlem2  9299  axpowndlem4  9301  axpownd  9302  axregndlem2  9304  axregnd  9305  axinfndlem1  9306  axinfnd  9307  zfcndrep  9315  zfcndinf  9319  dedekind  10079  dedekindle  10080  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  fsuppmapnn0fiubex  12654  nfsum1  14268  nfsum  14269  fsum2dlem  14343  fsum00  14371  nfcprod1  14479  nfcprod  14480  fprod2dlem  14549  fprodsplitf  14558  fprodsplit1f  14560  fprodle  14566  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  mreexexd  16131  mreexexdOLD  16132  acsmapd  17001  gsum2d2lem  18195  dprd2d2  18266  gsummoncoe1  19495  gsummatr01lem4  20283  cpmatmcllem  20342  pmatcollpwfi  20406  cayleyhamilton1  20516  neiptopnei  20746  neiptopreu  20747  neitr  20794  iunconlem  21040  iuncon  21041  ptcnplem  21234  ptcnp  21235  xkocnv  21427  isfildlem  21471  utopsnneiplem  21861  isucn2  21893  cfilucfil  22174  restmetu  22185  ovolfiniun  23076  ovoliunlem3  23079  ovoliunnul  23082  volfiniun  23122  itg2splitlem  23321  itg2split  23322  isibl2  23339  nfitg  23347  cbvitg  23348  limciun  23464  istrkg2ld  25159  chirred  28638  spc2ed  28696  mo5f  28708  rmo3f  28719  rmo4fOLD  28720  foresf1o  28727  cbvdisjf  28767  disjabrex  28777  disjabrexf  28778  funimass4f  28818  fmptcof2  28839  fcomptf  28840  acunirnmpt2  28842  acunirnmpt2f  28843  aciunf1lem  28844  funcnv4mpt  28853  cnvoprab  28886  f1od2  28887  fpwrelmap  28896  xrofsup  28923  nn0min  28954  2sqmo  28980  isarchiofld  29148  reff  29234  locfinreflem  29235  cmpcref  29245  ordtconlem1  29298  esumcl  29419  gsumesum  29448  esumlub  29449  esumcst  29452  esumrnmpt2  29457  esumfzf  29458  esumfsup  29459  hasheuni  29474  esumcvg  29475  esumgect  29479  esumcvgre  29480  esum2dlem  29481  esum2d  29482  esumiun  29483  ldsysgenld  29550  sigapildsyslem  29551  sigapildsys  29552  ldgenpisyslem1  29553  measvunilem  29602  measvunilem0  29603  measvuni  29604  measinblem  29610  voliune  29619  volfiniune  29620  volmeas  29621  oms0  29686  omssubadd  29689  eulerpartlemgvv  29765  dstrvprob  29860  bnj919  30091  bnj1146  30116  bnj1379  30155  bnj849  30249  bnj916  30257  bnj964  30267  bnj1014  30284  bnj1123  30308  bnj1228  30333  bnj1307  30345  bnj1321  30349  bnj1398  30356  bnj1408  30358  bnj1444  30365  bnj1445  30366  bnj1446  30367  bnj1449  30370  bnj1467  30376  bnj1463  30377  bnj1489  30378  bnj1491  30379  bnj1312  30380  bnj1525  30391  cvmcov  30499  iota5f  30861  axextdist  30949  axext4dist  30950  trpredmintr  30975  nfwlim  31012  frrlem4  31027  finminlem  31482  bj-axrep3  31978  bj-axrep4  31979  bj-axrep5  31980  bj-dvelimdv  32027  isbasisrelowllem1  32379  isbasisrelowllem2  32380  wl-cbvalnaed  32498  wl-2sb6d  32520  wl-sbalnae  32524  wl-mo2tf  32532  wl-eutf  32534  wl-ax11-lem3  32543  phpreu  32563  poimirlem26  32605  poimirlem27  32606  heicant  32614  mbfposadd  32627  ftc1anclem5  32659  indexdom  32699  filbcmb  32705  sdclem2  32708  sdclem1  32709  fdc1  32712  riotasv2d  33261  riotasv2s  33262  nfded2  33273  glbconxN  33682  pmapglb2xN  34076  cdlemefs32sn1aw  34720  mzpsubmpt  36324  mzpexpmpt  36326  eq0rabdioph  36358  eqrabdioph  36359  setindtr  36609  ss2iundf  36970  binomcxplemnotnn0  37577  iunconlem2  38193  elunif  38198  rspcegf  38205  fnchoice  38211  refsumcn  38212  rfcnnnub  38218  uzwo4  38246  fiiuncl  38259  rspcef  38267  cbvmpt22  38305  cbvmpt21  38306  disjf1  38364  wessf1ornlem  38366  disjrnmpt2  38370  disjf1o  38373  fompt  38374  disjinfi  38375  choicefi  38387  axccdom  38411  dmrelrnrel  38414  axccd  38424  upbdrech  38460  ssfiunibd  38464  supxrgere  38490  supxrgelem  38494  supxrge  38495  xralrple2  38511  infxr  38524  infxrunb2  38525  xrralrecnnle  38543  xrralrecnnge  38554  iccshift  38591  iooshift  38595  iooiinicc  38616  iooiinioc  38630  fsumclf  38633  fsumsplitf  38634  fsummulc1f  38635  fsumsplit1  38639  fsumf1of  38641  fsumreclf  38643  fsumlessf  38644  fmul01  38647  fmuldfeqlem1  38649  fmuldfeq  38650  fmul01lt1lem1  38651  fmul01lt1lem2  38652  fprodexp  38661  mccl  38665  fprodcnlem  38666  fprodcn  38667  climmulf  38671  climexp  38672  climsuse  38675  climrecf  38676  climinff  38678  climaddf  38682  mullimc  38683  islptre  38686  climf  38689  mullimcf  38690  rexlim2d  38692  idlimc  38693  limcperiod  38695  limcrecl  38696  islpcn  38706  limsupre  38708  limcleqr  38711  addlimc  38715  limclner  38718  climsubmpt  38727  climreclf  38731  climf2  38733  climeldmeqmpt  38735  clim2f2  38737  climfveqmpt  38738  fnlimfvre  38741  allbutfifvre  38742  climleltrp  38743  fnlimf  38745  fnlimabslt  38746  cncficcgt0  38774  cncfioobd  38783  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvmptmulf  38827  dvnmul  38833  dvmptfprodlem  38834  dvmptfprod  38835  dvnprodlem1  38836  dvnprodlem2  38837  iblsplitf  38862  itgperiod  38873  stoweidlem3  38896  stoweidlem26  38919  stoweidlem27  38920  stoweidlem29  38922  stoweidlem31  38924  stoweidlem34  38927  stoweidlem35  38928  stoweidlem36  38929  stoweidlem39  38932  stoweidlem42  38935  stoweidlem43  38936  stoweidlem44  38937  stoweidlem46  38939  stoweidlem48  38941  stoweidlem49  38942  stoweidlem51  38944  stoweidlem52  38945  stoweidlem53  38946  stoweidlem54  38947  stoweidlem55  38948  stoweidlem56  38949  stoweidlem57  38950  stoweidlem58  38951  stoweidlem59  38952  stoweidlem60  38953  stoweidlem61  38954  stoweidlem62  38955  stoweid  38956  wallispilem3  38960  stirlinglem13  38979  stirling  38982  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem31  39031  fourierdlem39  39039  fourierdlem48  39047  fourierdlem51  39050  fourierdlem53  39052  fourierdlem68  39067  fourierdlem71  39070  fourierdlem73  39072  fourierdlem80  39079  fourierdlem81  39080  fourierdlem86  39085  fourierdlem87  39086  fourierdlem93  39092  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  elaa2  39127  etransclem32  39159  salexct  39228  sge0revalmpt  39271  sge0f1o  39275  sge0lefi  39291  sge0resplit  39299  sge0lempt  39303  sge0iunmptlemre  39308  sge0fodjrnlem  39309  sge0iunmpt  39311  sge0ltfirpmpt2  39319  sge0isum  39320  sge0xp  39322  sge0isummpt2  39325  sge0xadd  39328  sge0pnffsumgt  39335  sge0gtfsumgt  39336  sge0uzfsumgt  39337  sge0reuz  39340  sge0reuzb  39341  iundjiun  39353  meadjiun  39359  ismeannd  39360  voliunsge0lem  39365  meaiininc  39377  caragenfiiuncl  39405  omeiunltfirp  39409  ovnsubaddlem2  39461  hoidmvval0  39477  hoidmvlelem1  39485  hoidmvlelem3  39487  hoidmvlelem5  39489  ovnlecvr2  39500  hspdifhsp  39506  hoiqssbllem2  39513  hoiqssbllem3  39514  hspmbllem2  39517  opnvonmbllem2  39523  hoimbl2  39555  vonhoire  39563  iinhoiicc  39565  iunhoiioolem  39566  iunhoiioo  39567  vonioo  39573  vonicc  39576  vonn0ioo2  39581  vonn0icc2  39583  salpreimagelt  39595  salpreimalegt  39597  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  preimageiingt  39607  preimaleiinlt  39608  salpreimagtge  39611  salpreimaltle  39612  salpreimalelt  39615  salpreimagtlt  39616  incsmflem  39628  issmflelem  39631  issmfle  39632  smfconst  39636  issmfgtlem  39642  issmfgt  39643  smfaddlem2  39650  smfadd  39651  decsmflem  39652  decsmf  39653  issmfgelem  39655  issmfge  39656  smflimlem2  39658  smflim  39663  smfresal  39673  smfrec  39674  smfmullem4  39679  smfmul  39680  nfdfat  39859  iccelpart  39971  2zrngmmgm  41736  opeliun2xp  41904  cbvmpt2x2  41907  ovmpt2rdxf  41910  setrec1  42237  aacllem  42356
  Copyright terms: Public domain W3C validator