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

Theorem nfan 1895
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
StepHypRef Expression
1 nfan.1 . . . 4 𝑥𝜑
21a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
3 nfan.2 . . . 4 𝑥𝜓
43a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜓)
52, 4nfand 1893 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65mptru 1541 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wa 395  wtru 1535  wnf 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779
This theorem is referenced by:  nfnan  1896  nf3an  1897  hban  2289  nfeqf  2375  nfald2  2439  2ax6elem  2464  nfsb4t  2493  nfeu1ALT  2578  eupicka  2625  mopick2  2628  2mo  2639  clelabOLD  2875  nfabd2  2924  2ralbida  3275  r19.12  3306  r19.12OLD  3307  reean  3308  ralcom2  3368  cbvrmow  3400  nfrmow  3404  nfreuw  3405  cbvreuwOLD  3407  cbvreu  3419  cbvrabw  3462  nfrabw  3463  cbvrab  3468  ceqsex2  3525  vtocl2gaf  3563  spc2ed  3586  rspce  3596  eqvincf  3634  elrabf  3676  elrab3t  3679  rexab2  3692  morex  3712  reu2  3718  rmo3f  3727  reu2eqd  3729  sbc2iegf  3855  reu8nf  3867  rmo2  3877  rmo3  3879  csbiebt  3919  csbie2t  3930  cbvrabcsfw  3933  cbvreucsf  3936  cbvrabcsf  3937  reusngf  4672  rexreusng  4679  reuprg0  4702  rabsnifsb  4722  nfop  4885  nfopd  4886  eluniab  4917  iuneqconst  5002  cbvopab  5214  cbvopab1  5217  cbvopab1g  5218  cbvopab2  5219  cbvopab1s  5220  mpteq12f  5230  nfmpt  5249  cbvmptf  5251  cbvmptfg  5252  axrep3  5283  axrep4  5284  axrep5  5285  reusv2lem3  5394  axprlem4  5420  axprlem5  5421  nfpo  5589  nfso  5590  nffr  5646  nfwe  5648  nfxp  5705  opeliunxp  5739  nfco  5862  elrnmpt1  5954  nfimad  6066  reuop  6291  iota2  6531  nffun  6570  imadif  6631  nffn  6647  nff  6712  nff1  6785  nffo  6804  nff1o  6831  nffvd  6903  fv3  6909  funimassd  6959  fvmptdf  7005  fompt  7122  f1ossf1o  7131  fmptco  7132  fsnex  7286  nfiso  7324  nfriotadw  7378  cbvriotaw  7379  nfriotad  7382  cbvriota  7384  riota2df  7394  riota5f  7399  oprabv  7474  nfoprab  7478  mpoeq123  7486  nfmpo  7496  cbvoprab1  7501  cbvoprab2  7502  cbvoprab12  7503  cbvoprab3  7505  cbvmpox  7507  ovmpodxf  7565  elovmporab  7661  elovmporab1w  7662  elovmporab1  7663  onminex  7799  peano5OLD  7894  fiun  7940  f1iun  7941  opabex3d  7963  opabex3rd  7964  opabex3  7965  dfoprab4f  8054  fmpox  8065  opeliunxp2f  8209  nffrecs  8282  frrlem4  8288  nfwrecsOLD  8316  wfrlem4OLD  8326  tfr3  8413  tz7.49  8459  erovlem  8825  nfixpw  8928  nfixp  8929  nfixp1  8930  xpf1o  9157  nneneq  9227  nneneqOLD  9239  ac6sfi  9305  nfoi  9531  wdom2d  9597  infpssrlem4  10323  hsmexlem2  10444  hsmexlem4  10446  domtriomlem  10459  axdc3lem2  10468  axdc4lem  10472  zorn2lem4  10516  zorn2lem5  10517  konigthlem  10585  axextnd  10608  axrepndlem2  10610  axrepnd  10611  axunnd  10613  axpowndlem2  10615  axpowndlem4  10617  axpownd  10618  axregndlem2  10620  axregnd  10621  axinfndlem1  10622  axinfnd  10623  zfcndrep  10631  zfcndinf  10635  dedekind  11401  dedekindle  11402  fsuppmapnn0fiublem  13981  fsuppmapnn0fiub  13982  fsuppmapnn0fiubex  13983  reuccatpfxs1  14723  nfsum1  15662  nfsum  15663  fsumclf  15710  fsumsplitf  15714  fsumsplit1  15717  fsum2dlem  15742  fsum00  15770  nfcprod1  15880  nfcprod  15881  fprod2dlem  15950  fprodsplitf  15958  fprodsplit1f  15960  fprodle  15966  lcmfunsnlem1  16601  lcmfunsnlem2lem1  16602  lcmfunsnlem2  16604  mreexexd  17621  acsmapd  18539  gsum2d2lem  19921  dprd2d2  19994  gsummoncoe1  22220  gsummatr01lem4  22553  cpmatmcllem  22613  cayleyhamilton1  22787  neiptopnei  23029  neiptopreu  23030  neitr  23077  iunconnlem  23324  iunconn  23325  ptcnplem  23518  ptcnp  23519  xkocnv  23711  isfildlem  23754  utopsnneiplem  24145  isucn2  24177  cfilucfil  24461  restmetu  24472  ovolfiniun  25423  ovoliunlem3  25426  ovoliunnul  25429  volfiniun  25469  itg2splitlem  25671  itg2split  25672  isibl2  25689  nfitg  25697  cbvitg  25698  limciun  25816  2sqmo  27363  2sqreulem4  27380  istrkg2ld  28257  chirred  32198  sbc2iedf  32258  rspc2daf  32259  opreu2reuALT  32268  mo5f  32280  foresf1o  32293  iinabrex  32352  cbvdisjf  32354  disjabrex  32365  disjabrexf  32366  funimass4f  32415  2ndresdju  32428  fmptcof2  32436  fcomptf  32437  acunirnmpt2  32439  acunirnmpt2f  32440  aciunf1lem  32441  funcnv4mpt  32448  fnpreimac  32450  cnvoprabOLD  32496  f1od2  32497  fpwrelmap  32509  xrofsup  32531  nn0min  32577  fprodex01  32582  fsumiunle  32586  isarchiofld  33026  nsgqusf1olem1  33117  nsgqusf1olem3  33119  elrspunidl  33133  fedgmullem2  33314  irngnzply1  33355  reff  33430  locfinreflem  33431  cmpcref  33441  zarclsiin  33462  zarcmplem  33472  ordtconnlem1  33515  prodindf  33632  esumcl  33639  gsumesum  33668  esumlub  33669  esumcst  33672  esumrnmpt2  33677  esumfzf  33678  esumfsup  33679  hasheuni  33694  esumcvg  33695  esumgect  33699  esumcvgre  33700  esum2dlem  33701  esum2d  33702  esumiun  33703  ldsysgenld  33769  sigapildsyslem  33770  sigapildsys  33771  ldgenpisyslem1  33772  measvunilem  33821  measvunilem0  33822  measvuni  33823  measinblem  33829  voliune  33838  volfiniune  33839  volmeas  33840  oms0  33907  omssubadd  33910  eulerpartlemgvv  33986  dstrvprob  34081  breprexplema  34252  bnj919  34388  bnj1146  34412  bnj1379  34451  bnj849  34546  bnj916  34554  bnj964  34564  bnj1014  34582  bnj1123  34607  bnj1228  34632  bnj1307  34644  bnj1321  34648  bnj1398  34655  bnj1408  34657  bnj1444  34664  bnj1445  34665  bnj1446  34666  bnj1449  34669  bnj1467  34675  bnj1463  34676  bnj1489  34677  bnj1491  34678  bnj1312  34679  bnj1525  34690  fineqvrep  34705  cvmcov  34863  iota5f  35308  axextdist  35385  axextbdist  35386  nfwlim  35408  finminlem  35792  bj-dvelimdv  36318  bj-opabco  36657  isbasisrelowllem1  36824  isbasisrelowllem2  36825  fvineqsneu  36880  fvineqsneq  36881  wl-cbvalnaed  36989  wl-2sb6d  37014  wl-sbalnae  37018  wl-mo2tf  37027  wl-eutf  37029  wl-ax11-lem3  37043  phpreu  37066  poimirlem26  37108  poimirlem27  37109  heicant  37117  mbfposadd  37129  ftc1anclem5  37159  indexdom  37196  filbcmb  37202  sdclem2  37204  sdclem1  37205  fdc1  37208  riotasv2d  38418  riotasv2s  38419  nfded2  38429  glbconxN  38840  pmapglb2xN  39234  cdlemefs32sn1aw  39876  mzpsubmpt  42135  mzpexpmpt  42137  eq0rabdioph  42168  eqrabdioph  42169  setindtr  42417  unielss  42618  nadd1suc  42793  naddsuc2  42794  ss2iundf  43061  scottabf  43649  mnuprdlem4  43684  ismnushort  43710  binomcxplemnotnn0  43765  iunconnlem2  44346  elunif  44350  rspcegf  44357  fnchoice  44363  refsumcn  44364  rfcnnnub  44370  uzwo4  44389  fiiuncl  44401  cbvmpo2  44435  cbvmpo1  44436  iinssiin  44467  disjf1  44528  disjrnmpt2  44533  disjf1o  44536  disjinfi  44537  choicefi  44545  axccdom  44567  dmrelrnrel  44571  axccd  44574  rnmptbddlem  44592  rnmptbd2lem  44596  infnsuprnmpt  44598  rnmptbdlem  44603  rnmptssbi  44609  upbdrech  44659  ssfiunibd  44663  supxrgere  44687  supxrgelem  44691  supxrge  44692  xralrple2  44708  infxr  44721  infxrunb2  44722  xrralrecnnle  44737  xrralrecnnge  44744  supxrunb3  44753  supxrleubrnmpt  44760  infleinf2  44768  unb2ltle  44769  rexabslelem  44772  suprleubrnmpt  44776  uzub  44785  supminfrnmpt  44799  supxrleubrnmptf  44805  infxrgelbrnmpt  44808  infrpgernmpt  44819  monoordxr  44837  monoord2xr  44839  caucvgbf  44844  cvgcaule  44846  iccshift  44875  iooshift  44879  iooiinicc  44899  iooiinioc  44913  fsummulc1f  44931  fsumf1of  44934  fsumreclf  44936  fsumlessf  44937  fmul01  44940  fmuldfeqlem1  44942  fmuldfeq  44943  fmul01lt1lem1  44944  fmul01lt1lem2  44945  fprodexp  44954  mccl  44958  fprodcnlem  44959  fprodcn  44960  climmulf  44964  climexp  44965  climsuse  44968  climrecf  44969  climinff  44971  climaddf  44975  mullimc  44976  islptre  44979  climf  44982  mullimcf  44983  rexlim2d  44985  idlimc  44986  limcperiod  44988  limcrecl  44989  islpcn  44999  limsupre  45001  limcleqr  45004  addlimc  45008  limclner  45011  climsubmpt  45020  climreclf  45024  climf2  45026  climeldmeqmpt  45028  clim2f2  45030  climfveqmpt  45031  fnlimfvre  45034  allbutfifvre  45035  climleltrp  45036  fnlimf  45038  fnlimabslt  45039  climfveqf  45040  climfveqmpt3  45042  climeldmeqf  45043  climeqf  45048  climeldmeqmpt3  45049  limsuppnfd  45062  limsupub  45064  climinf2lem  45066  climinf2  45067  limsuppnf  45071  limsupubuz  45073  climinf2mpt  45074  climinfmpt  45075  climinf3  45076  limsupmnflem  45080  limsupequz  45083  limsupre2  45085  limsupmnfuzlem  45086  limsupequzmptf  45091  limsupre3  45093  limsupre3uzlem  45095  limsupreuzmpt  45099  climisp  45106  lmbr3  45107  climrescn  45108  climxrrelem  45109  climxrre  45110  limsupub2  45172  liminflbuz2  45175  xlimmnfvlem2  45193  xlimmnfv  45194  xlimpnfvlem2  45197  xlimpnfv  45198  xlimmnfmpt  45203  xlimpnfmpt  45204  climxlim2lem  45205  cncficcgt0  45248  cncfioobd  45257  fprodsubrecnncnvlem  45267  fprodaddrecnncnvlem  45269  dvmptmulf  45297  dvnmul  45303  dvmptfprodlem  45304  dvmptfprod  45305  dvnprodlem1  45306  dvnprodlem2  45307  iblsplitf  45330  itgperiod  45341  stoweidlem3  45363  stoweidlem26  45386  stoweidlem27  45387  stoweidlem29  45389  stoweidlem31  45391  stoweidlem34  45394  stoweidlem35  45395  stoweidlem36  45396  stoweidlem39  45399  stoweidlem42  45402  stoweidlem43  45403  stoweidlem44  45404  stoweidlem46  45406  stoweidlem48  45408  stoweidlem49  45409  stoweidlem51  45411  stoweidlem52  45412  stoweidlem53  45413  stoweidlem54  45414  stoweidlem55  45415  stoweidlem56  45416  stoweidlem57  45417  stoweidlem58  45418  stoweidlem59  45419  stoweidlem60  45420  stoweidlem61  45421  stoweidlem62  45422  stoweid  45423  wallispilem3  45427  stirlinglem13  45446  stirling  45449  fourierdlem16  45483  fourierdlem21  45488  fourierdlem22  45489  fourierdlem31  45498  fourierdlem39  45506  fourierdlem48  45514  fourierdlem51  45517  fourierdlem68  45534  fourierdlem71  45537  fourierdlem73  45539  fourierdlem80  45546  fourierdlem81  45547  fourierdlem86  45552  fourierdlem87  45553  fourierdlem93  45559  fourierdlem94  45560  fourierdlem103  45569  fourierdlem104  45570  fourierdlem112  45578  fourierdlem113  45579  elaa2  45594  etransclem32  45626  salexct  45694  sge0revalmpt  45738  sge0f1o  45742  sge0lefi  45758  sge0resplit  45766  sge0lempt  45770  sge0iunmptlemre  45775  sge0fodjrnlem  45776  sge0iunmpt  45778  sge0ltfirpmpt2  45786  sge0isum  45787  sge0xp  45789  sge0isummpt2  45792  sge0xadd  45795  sge0pnffsumgt  45802  sge0gtfsumgt  45803  sge0uzfsumgt  45804  sge0reuz  45807  sge0reuzb  45808  iundjiun  45820  meadjiun  45826  ismeannd  45827  voliunsge0lem  45832  meaiunincf  45843  meaiuninc3v  45844  meaiuninc3  45845  meaiininc  45847  caragenfiiuncl  45875  omeiunltfirp  45879  ovnsubaddlem2  45931  hoidmvval0  45947  hoidmvlelem1  45955  hoidmvlelem3  45957  hoidmvlelem5  45959  ovnlecvr2  45970  hspdifhsp  45976  hoiqssbllem2  45983  hoiqssbllem3  45984  hspmbllem2  45987  opnvonmbllem2  45993  hoimbl2  46025  vonhoire  46032  iinhoiicc  46034  iunhoiioolem  46035  iunhoiioo  46036  vonioo  46042  vonicc  46045  vonn0ioo2  46050  vonn0icc2  46052  salpreimagelt  46067  salpreimalegt  46069  pimincfltioc  46076  pimdecfgtioo  46077  pimincfltioo  46078  preimageiingt  46080  preimaleiinlt  46081  salpreimagtge  46085  salpreimaltle  46086  salpreimalelt  46089  salpreimagtlt  46090  incsmflem  46101  issmflelem  46104  issmfle  46105  smfconst  46109  issmfgtlem  46115  issmfgt  46116  smfaddlem2  46124  smfadd  46125  decsmflem  46126  decsmf  46127  issmfgelem  46129  issmfge  46130  smflimlem2  46132  smflim  46137  smfresal  46148  smfrec  46149  smfmullem4  46154  smfmul  46155  smfpimcc  46168  smflimmpt  46170  smfsuplem1  46171  smfsupmpt  46175  smfsupxr  46176  smfinflem  46177  smfinfmpt  46179  smflimsuplem5  46184  smflimsuplem7  46186  smflimsuplem8  46187  smflimsupmpt  46189  smfliminflem  46190  smfliminfmpt  46192  smfpimne2  46200  fsupdm  46202  smfsupdmmbllem  46204  finfdm  46206  smfinfdmmbllem  46208  or2expropbilem2  46387  or2expropbi  46388  cfsetsnfsetf  46412  2reu8i  46465  nfdfat  46479  iccelpart  46745  ichnfim  46776  ich2exprop  46783  ichreuopeq  46785  sprsymrelfo  46809  reupr  46834  reuopreuprim  46838  2zrngmmgm  47286  opeliun2xp  47368  cbvmpox2  47371  ovmpordxf  47374  1arymaptfo  47688  2arymaptfo  47699  setrec1  48094  pgindnf  48119  aacllem  48206
  Copyright terms: Public domain W3C validator