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

Theorem nfan 1977
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 1975 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65trud 1642 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wa 383  wtru 1633  wnf 1857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859
This theorem is referenced by:  nfnan  1979  nf3an  1980  hban  2275  nfeqf  2446  nfald2  2471  nfsb4t  2526  2ax6elem  2586  eupicka  2675  mopick2  2678  2mo  2689  axbnd  2739  clelab  2886  nfabd2  2922  2ralbida  3125  r19.29an  3215  ralcom2  3242  reean  3244  cbvreu  3308  cbvrab  3338  ceqsex2  3384  vtocl2gaf  3413  rspce  3444  eqvincf  3470  elrabf  3500  elrab3t  3503  rexab2  3514  morex  3531  reu2  3535  reu2eqd  3544  sbc2iegf  3645  reu8nf  3657  rmo2  3667  rmo3  3669  csbiebt  3694  csbie2t  3703  cbvreucsf  3708  cbvrabcsf  3709  rabsnifsb  4401  nfop  4569  nfopd  4570  eluniab  4599  dfnfc2OLD  4607  nfopab  4870  cbvopab  4873  cbvopab1  4875  cbvopab2  4876  cbvopab1s  4877  mpteq12f  4883  nfmpt  4898  cbvmptf  4900  cbvmpt  4901  axrep3  4926  axrep4  4927  axrep5  4928  reusv2lem2OLD  5019  reusv2lem3  5020  nfpo  5192  nfso  5193  nffr  5240  nfwe  5242  nfxp  5299  opeliunxp  5327  nfco  5443  elrnmpt1  5529  nfimad  5633  elsnxpOLD  5839  iota2  6038  nffun  6072  imadif  6134  nffn  6148  nff  6202  nff1  6260  nffo  6275  nff1o  6296  nffvd  6361  fv3  6367  fmptco  6559  fsnex  6701  nfiso  6735  nfriotad  6782  cbvriota  6784  riota2df  6794  riota5f  6799  oprabv  6868  nfoprab  6872  mpt2eq123  6879  nfmpt2  6889  cbvoprab1  6892  cbvoprab2  6893  cbvoprab12  6894  cbvoprab3  6896  cbvmpt2x  6898  ovmpt2dxf  6951  elovmpt2rab  7045  elovmpt2rab1  7046  onminex  7172  peano5  7254  fun11iun  7291  opabex3d  7310  opabex3  7311  dfoprab4f  7393  fmpt2x  7404  opeliunxp2f  7505  nfwrecs  7578  wfrlem4  7587  tfr3  7664  tz7.49  7709  erovlem  8010  nfixp  8093  nfixp1  8094  xpf1o  8287  nneneq  8308  ac6sfi  8369  nfoi  8584  wdom2d  8650  infpssrlem4  9320  hsmexlem2  9441  hsmexlem4  9443  domtriomlem  9456  axdc3lem2  9465  axdc4lem  9469  zorn2lem4  9513  zorn2lem5  9514  konigthlem  9582  axextnd  9605  axrepndlem2  9607  axrepnd  9608  axunnd  9610  axpowndlem2  9612  axpowndlem4  9614  axpownd  9615  axregndlem2  9617  axregnd  9618  axinfndlem1  9619  axinfnd  9620  zfcndrep  9628  zfcndinf  9632  dedekind  10392  dedekindle  10393  fsuppmapnn0fiublem  12983  fsuppmapnn0fiub  12984  fsuppmapnn0fiubOLD  12985  fsuppmapnn0fiubex  12986  reuccats1  13680  nfsum1  14619  nfsum  14620  fsumsplitf  14671  fsum2dlem  14700  fsum00  14729  nfcprod1  14839  nfcprod  14840  fprod2dlem  14909  fprodsplitf  14918  fprodsplit1f  14920  fprodle  14926  lcmfunsnlem1  15552  lcmfunsnlem2lem1  15553  lcmfunsnlem2  15555  mreexexd  16510  acsmapd  17379  gsum2d2lem  18572  dprd2d2  18643  gsummoncoe1  19876  gsummatr01lem4  20666  cpmatmcllem  20725  pmatcollpwfi  20789  cayleyhamilton1  20899  neiptopnei  21138  neiptopreu  21139  neitr  21186  iunconnlem  21432  iunconn  21433  ptcnplem  21626  ptcnp  21627  xkocnv  21819  isfildlem  21862  utopsnneiplem  22252  isucn2  22284  cfilucfil  22565  restmetu  22576  ovolfiniun  23469  ovoliunlem3  23472  ovoliunnul  23475  volfiniun  23515  itg2splitlem  23714  itg2split  23715  isibl2  23732  nfitg  23740  cbvitg  23741  limciun  23857  istrkg2ld  25558  chirred  29563  spc2ed  29621  mo5f  29633  rmo3f  29643  rmo4fOLD  29644  foresf1o  29650  cbvdisjf  29692  disjabrex  29702  disjabrexf  29703  funimass4f  29746  fmptcof2  29766  fcomptf  29767  acunirnmpt2  29769  acunirnmpt2f  29770  aciunf1lem  29771  funcnv4mpt  29779  cnvoprabOLD  29807  f1od2  29808  fpwrelmap  29817  xrofsup  29842  nn0min  29876  fprodex01  29880  fsumiunle  29884  2sqmo  29958  isarchiofld  30126  reff  30215  locfinreflem  30216  cmpcref  30226  ordtconnlem1  30279  prodindf  30394  esumcl  30401  gsumesum  30430  esumlub  30431  esumcst  30434  esumrnmpt2  30439  esumfzf  30440  esumfsup  30441  hasheuni  30456  esumcvg  30457  esumgect  30461  esumcvgre  30462  esum2dlem  30463  esum2d  30464  esumiun  30465  ldsysgenld  30532  sigapildsyslem  30533  sigapildsys  30534  ldgenpisyslem1  30535  measvunilem  30584  measvunilem0  30585  measvuni  30586  measinblem  30592  voliune  30601  volfiniune  30602  volmeas  30603  oms0  30668  omssubadd  30671  eulerpartlemgvv  30747  dstrvprob  30842  breprexplema  31017  bnj919  31144  bnj1146  31169  bnj1379  31208  bnj849  31302  bnj916  31310  bnj964  31320  bnj1014  31337  bnj1123  31361  bnj1228  31386  bnj1307  31398  bnj1321  31402  bnj1398  31409  bnj1408  31411  bnj1444  31418  bnj1445  31419  bnj1446  31420  bnj1449  31423  bnj1467  31429  bnj1463  31430  bnj1489  31431  bnj1491  31432  bnj1312  31433  bnj1525  31444  cvmcov  31552  iota5f  31913  axextdist  32010  axext4dist  32011  trpredmintr  32036  nfwlim  32073  nffrecs  32084  frrlem4  32089  finminlem  32618  bj-axrep3  33096  bj-axrep4  33097  bj-axrep5  33098  bj-dvelimdv  33140  isbasisrelowllem1  33514  isbasisrelowllem2  33515  wl-cbvalnaed  33632  wl-2sb6d  33654  wl-sbalnae  33658  wl-mo2tf  33666  wl-eutf  33668  wl-ax11-lem3  33677  phpreu  33706  poimirlem26  33748  poimirlem27  33749  heicant  33757  mbfposadd  33770  ftc1anclem5  33802  indexdom  33842  filbcmb  33848  sdclem2  33851  sdclem1  33852  fdc1  33855  riotasv2d  34746  riotasv2s  34747  nfded2  34758  glbconxN  35167  pmapglb2xN  35561  cdlemefs32sn1aw  36204  mzpsubmpt  37808  mzpexpmpt  37810  eq0rabdioph  37842  eqrabdioph  37843  setindtr  38093  ss2iundf  38453  binomcxplemnotnn0  39057  iunconnlem2  39670  elunif  39674  rspcegf  39681  fnchoice  39687  refsumcn  39688  rfcnnnub  39694  uzwo4  39720  fiiuncl  39733  cbvmpt22  39776  cbvmpt21  39777  iinssiin  39811  ralimda  39825  disjf1  39868  wessf1ornlem  39870  disjrnmpt2  39874  disjf1o  39877  fompt  39878  disjinfi  39879  choicefi  39891  axccdom  39915  dmrelrnrel  39918  axccd  39928  funimassd  39930  rnmptbddlem  39954  rnmptbd2lem  39962  infnsuprnmpt  39964  rnmptbdlem  39969  rnmptssbi  39976  upbdrech  40018  ssfiunibd  40022  supxrgere  40047  supxrgelem  40051  supxrge  40052  xralrple2  40068  infxr  40081  infxrunb2  40082  xrralrecnnle  40100  xrralrecnnge  40111  supxrunb3  40121  supxrleubrnmpt  40130  infleinf2  40139  unb2ltle  40140  rexabslelem  40143  suprleubrnmpt  40147  uzub  40156  supminfrnmpt  40170  supxrleubrnmptf  40178  infxrgelbrnmpt  40181  infrpgernmpt  40193  monoordxr  40211  monoord2xr  40213  iccshift  40247  iooshift  40251  iooiinicc  40272  iooiinioc  40286  fsumclf  40304  fsummulc1f  40305  fsumsplit1  40307  fsumf1of  40309  fsumreclf  40311  fsumlessf  40312  fmul01  40315  fmuldfeqlem1  40317  fmuldfeq  40318  fmul01lt1lem1  40319  fmul01lt1lem2  40320  fprodexp  40329  mccl  40333  fprodcnlem  40334  fprodcn  40335  climmulf  40339  climexp  40340  climsuse  40343  climrecf  40344  climinff  40346  climaddf  40350  mullimc  40351  islptre  40354  climf  40357  mullimcf  40358  rexlim2d  40360  idlimc  40361  limcperiod  40363  limcrecl  40364  islpcn  40374  limsupre  40376  limcleqr  40379  addlimc  40383  limclner  40386  climsubmpt  40395  climreclf  40399  climf2  40401  climeldmeqmpt  40403  clim2f2  40405  climfveqmpt  40406  fnlimfvre  40409  allbutfifvre  40410  climleltrp  40411  fnlimf  40413  fnlimabslt  40414  climfveqf  40415  climfveqmpt3  40417  climeldmeqf  40418  climeqf  40423  climeldmeqmpt3  40424  limsuppnfd  40437  limsupub  40439  climinf2lem  40441  climinf2  40442  limsuppnf  40446  limsupubuz  40448  climinf2mpt  40449  climinfmpt  40450  climinf3  40451  limsupmnflem  40455  limsupequz  40458  limsupre2  40460  limsupmnfuzlem  40461  limsupequzmptf  40466  limsupre3  40468  limsupre3uzlem  40470  limsupreuzmpt  40474  climisp  40481  lmbr3  40482  climrescn  40483  climxrrelem  40484  climxrre  40485  xlimmnfvlem2  40562  xlimmnfv  40563  xlimpnfvlem2  40566  xlimpnfv  40567  xlimmnfmpt  40572  xlimpnfmpt  40573  climxlim2lem  40574  cncficcgt0  40604  cncfioobd  40613  fprodsubrecnncnvlem  40624  fprodaddrecnncnvlem  40626  dvmptmulf  40655  dvnmul  40661  dvmptfprodlem  40662  dvmptfprod  40663  dvnprodlem1  40664  dvnprodlem2  40665  iblsplitf  40689  itgperiod  40700  stoweidlem3  40723  stoweidlem26  40746  stoweidlem27  40747  stoweidlem29  40749  stoweidlem31  40751  stoweidlem34  40754  stoweidlem35  40755  stoweidlem36  40756  stoweidlem39  40759  stoweidlem42  40762  stoweidlem43  40763  stoweidlem44  40764  stoweidlem46  40766  stoweidlem48  40768  stoweidlem49  40769  stoweidlem51  40771  stoweidlem52  40772  stoweidlem53  40773  stoweidlem54  40774  stoweidlem55  40775  stoweidlem56  40776  stoweidlem57  40777  stoweidlem58  40778  stoweidlem59  40779  stoweidlem60  40780  stoweidlem61  40781  stoweidlem62  40782  stoweid  40783  wallispilem3  40787  stirlinglem13  40806  stirling  40809  fourierdlem16  40843  fourierdlem21  40848  fourierdlem22  40849  fourierdlem31  40858  fourierdlem39  40866  fourierdlem48  40874  fourierdlem51  40877  fourierdlem53  40879  fourierdlem68  40894  fourierdlem71  40897  fourierdlem73  40899  fourierdlem80  40906  fourierdlem81  40907  fourierdlem86  40912  fourierdlem87  40913  fourierdlem93  40919  fourierdlem94  40920  fourierdlem103  40929  fourierdlem104  40930  fourierdlem112  40938  fourierdlem113  40939  elaa2  40954  etransclem32  40986  salexct  41055  sge0revalmpt  41098  sge0f1o  41102  sge0lefi  41118  sge0resplit  41126  sge0lempt  41130  sge0iunmptlemre  41135  sge0fodjrnlem  41136  sge0iunmpt  41138  sge0ltfirpmpt2  41146  sge0isum  41147  sge0xp  41149  sge0isummpt2  41152  sge0xadd  41155  sge0pnffsumgt  41162  sge0gtfsumgt  41163  sge0uzfsumgt  41164  sge0reuz  41167  sge0reuzb  41168  iundjiun  41180  meadjiun  41186  ismeannd  41187  voliunsge0lem  41192  meaiunincf  41203  meaiuninc3v  41204  meaiuninc3  41205  meaiininc  41207  caragenfiiuncl  41235  omeiunltfirp  41239  ovnsubaddlem2  41291  hoidmvval0  41307  hoidmvlelem1  41315  hoidmvlelem3  41317  hoidmvlelem5  41319  ovnlecvr2  41330  hspdifhsp  41336  hoiqssbllem2  41343  hoiqssbllem3  41344  hspmbllem2  41347  opnvonmbllem2  41353  hoimbl2  41385  vonhoire  41392  iinhoiicc  41394  iunhoiioolem  41395  iunhoiioo  41396  vonioo  41402  vonicc  41405  vonn0ioo2  41410  vonn0icc2  41412  salpreimagelt  41424  salpreimalegt  41426  pimincfltioc  41432  pimdecfgtioo  41433  pimincfltioo  41434  preimageiingt  41436  preimaleiinlt  41437  salpreimagtge  41440  salpreimaltle  41441  salpreimalelt  41444  salpreimagtlt  41445  incsmflem  41456  issmflelem  41459  issmfle  41460  smfconst  41464  issmfgtlem  41470  issmfgt  41471  smfaddlem2  41478  smfadd  41479  decsmflem  41480  decsmf  41481  issmfgelem  41483  issmfge  41484  smflimlem2  41486  smflim  41491  smfresal  41501  smfrec  41502  smfmullem4  41507  smfmul  41508  smfpimcc  41520  smflimmpt  41522  smfsuplem1  41523  smfsupmpt  41527  smfsupxr  41528  smfinflem  41529  smfinfmpt  41531  smflimsuplem5  41536  smflimsuplem7  41538  smflimsuplem8  41539  smflimsupmpt  41541  smfliminflem  41542  smfliminfmpt  41544  nfdfat  41716  iccelpart  41879  sprsymrelfo  42257  2zrngmmgm  42456  opeliun2xp  42621  cbvmpt2x2  42624  ovmpt2rdxf  42627  setrec1  42948  aacllem  43060
  Copyright terms: Public domain W3C validator