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

Theorem nfan 1825
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 1823 . 2 (⊤ → Ⅎ𝑥(𝜑𝜓))
65trud 1490 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wa 384  wtru 1481  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfnan  1827  nf3an  1828  hban  2124  nfeqf  2300  nfald2  2330  nfsb4t  2388  2ax6elem  2448  eupicka  2536  mopick2  2539  2mo  2550  axbnd  2600  clelab  2745  nfabd2  2780  2ralbida  2983  r19.29an  3072  ralcom2  3098  reean  3100  cbvreu  3161  cbvrab  3188  ceqsex2  3234  vtocl2gaf  3263  rspce  3294  eqvincf  3319  elrabf  3348  elrab3t  3350  rexab2  3360  morex  3377  reu2  3381  reu2eqd  3390  sbc2iegf  3491  rmo2  3512  rmo3  3514  csbiebt  3539  csbie2t  3548  cbvreucsf  3553  cbvrabcsf  3554  rabsnifsb  4234  nfop  4393  nfopd  4394  eluniab  4420  dfnfc2OLD  4428  rabasiun  4496  nfopab  4690  cbvopab  4693  cbvopab1  4695  cbvopab2  4696  cbvopab1s  4697  mpteq12f  4701  nfmpt  4716  cbvmptf  4718  cbvmpt  4719  axrep3  4744  axrep4  4745  axrep5  4746  reusv2lem2OLD  4840  reusv2lem3  4841  nfpo  5010  nfso  5011  nffr  5058  nfwe  5060  nfxp  5112  opeliunxp  5141  nfco  5257  elrnmpt1  5344  nfimad  5444  elsnxpOLD  5647  iota2  5846  nffun  5880  imadif  5941  nffn  5955  nff  6008  nff1  6066  nffo  6081  nff1o  6102  nffvd  6167  fv3  6173  fmptco  6362  fsnex  6503  nfiso  6537  nfriotad  6584  cbvriota  6586  riota2df  6596  riota5f  6601  oprabv  6668  nfoprab  6672  mpt2eq123  6679  nfmpt2  6689  cbvoprab1  6692  cbvoprab2  6693  cbvoprab12  6694  cbvoprab3  6696  cbvmpt2x  6698  ovmpt2dxf  6751  elovmpt2rab  6845  elovmpt2rab1  6846  onminex  6969  peano5  7051  fun11iun  7088  opabex3d  7106  opabex3  7107  dfoprab4f  7186  fmpt2x  7196  opeliunxp2f  7296  nfwrecs  7369  wfrlem4  7378  tfr3  7455  tz7.49  7500  erovlem  7803  nfixp  7887  nfixp1  7888  xpf1o  8082  nneneq  8103  ac6sfi  8164  nfoi  8379  wdom2d  8445  infpssrlem4  9088  hsmexlem2  9209  hsmexlem4  9211  domtriomlem  9224  axdc3lem2  9233  axdc4lem  9237  zorn2lem4  9281  zorn2lem5  9282  konigthlem  9350  axextnd  9373  axrepndlem2  9375  axrepnd  9376  axunnd  9378  axpowndlem2  9380  axpowndlem4  9382  axpownd  9383  axregndlem2  9385  axregnd  9386  axinfndlem1  9387  axinfnd  9388  zfcndrep  9396  zfcndinf  9400  dedekind  10160  dedekindle  10161  fsuppmapnn0fiublem  12745  fsuppmapnn0fiub  12746  fsuppmapnn0fiubOLD  12747  fsuppmapnn0fiubex  12748  nfsum1  14370  nfsum  14371  fsumsplitf  14421  fsum2dlem  14448  fsum00  14476  nfcprod1  14584  nfcprod  14585  fprod2dlem  14654  fprodsplitf  14663  fprodsplit1f  14665  fprodle  14671  lcmfunsnlem1  15293  lcmfunsnlem2lem1  15294  lcmfunsnlem2  15296  mreexexd  16248  mreexexdOLD  16249  acsmapd  17118  gsum2d2lem  18312  dprd2d2  18383  gsummoncoe1  19614  gsummatr01lem4  20404  cpmatmcllem  20463  pmatcollpwfi  20527  cayleyhamilton1  20637  neiptopnei  20876  neiptopreu  20877  neitr  20924  iunconnlem  21170  iunconn  21171  ptcnplem  21364  ptcnp  21365  xkocnv  21557  isfildlem  21601  utopsnneiplem  21991  isucn2  22023  cfilucfil  22304  restmetu  22315  ovolfiniun  23209  ovoliunlem3  23212  ovoliunnul  23215  volfiniun  23255  itg2splitlem  23455  itg2split  23456  isibl2  23473  nfitg  23481  cbvitg  23482  limciun  23598  istrkg2ld  25293  chirred  29142  spc2ed  29200  mo5f  29213  rmo3f  29224  rmo4fOLD  29225  foresf1o  29231  cbvdisjf  29271  disjabrex  29281  disjabrexf  29282  funimass4f  29321  fmptcof2  29340  fcomptf  29341  acunirnmpt2  29343  acunirnmpt2f  29344  aciunf1lem  29345  funcnv4mpt  29354  cnvoprab  29382  f1od2  29383  fpwrelmap  29392  xrofsup  29418  nn0min  29450  2sqmo  29476  isarchiofld  29644  reff  29730  locfinreflem  29731  cmpcref  29741  ordtconnlem1  29794  esumcl  29915  gsumesum  29944  esumlub  29945  esumcst  29948  esumrnmpt2  29953  esumfzf  29954  esumfsup  29955  hasheuni  29970  esumcvg  29971  esumgect  29975  esumcvgre  29976  esum2dlem  29977  esum2d  29978  esumiun  29979  ldsysgenld  30046  sigapildsyslem  30047  sigapildsys  30048  ldgenpisyslem1  30049  measvunilem  30098  measvunilem0  30099  measvuni  30100  measinblem  30106  voliune  30115  volfiniune  30116  volmeas  30117  oms0  30182  omssubadd  30185  eulerpartlemgvv  30261  dstrvprob  30356  bnj919  30598  bnj1146  30623  bnj1379  30662  bnj849  30756  bnj916  30764  bnj964  30774  bnj1014  30791  bnj1123  30815  bnj1228  30840  bnj1307  30852  bnj1321  30856  bnj1398  30863  bnj1408  30865  bnj1444  30872  bnj1445  30873  bnj1446  30874  bnj1449  30877  bnj1467  30883  bnj1463  30884  bnj1489  30885  bnj1491  30886  bnj1312  30887  bnj1525  30898  cvmcov  31006  iota5f  31368  axextdist  31459  axext4dist  31460  trpredmintr  31485  nfwlim  31522  frrlem4  31537  finminlem  32007  bj-axrep3  32486  bj-axrep4  32487  bj-axrep5  32488  bj-dvelimdv  32532  isbasisrelowllem1  32874  isbasisrelowllem2  32875  wl-cbvalnaed  32990  wl-2sb6d  33012  wl-sbalnae  33016  wl-mo2tf  33024  wl-eutf  33026  wl-ax11-lem3  33035  phpreu  33064  poimirlem26  33106  poimirlem27  33107  heicant  33115  mbfposadd  33128  ftc1anclem5  33160  indexdom  33200  filbcmb  33206  sdclem2  33209  sdclem1  33210  fdc1  33213  riotasv2d  33762  riotasv2s  33763  nfded2  33774  glbconxN  34183  pmapglb2xN  34577  cdlemefs32sn1aw  35221  mzpsubmpt  36825  mzpexpmpt  36827  eq0rabdioph  36859  eqrabdioph  36860  setindtr  37110  ss2iundf  37471  binomcxplemnotnn0  38076  iunconnlem2  38693  elunif  38697  rspcegf  38704  fnchoice  38710  refsumcn  38711  rfcnnnub  38717  uzwo4  38743  fiiuncl  38756  cbvmpt22  38799  cbvmpt21  38800  iinssiin  38837  ralimda  38852  disjf1  38878  wessf1ornlem  38880  disjrnmpt2  38884  disjf1o  38887  fompt  38888  disjinfi  38889  choicefi  38901  axccdom  38925  dmrelrnrel  38928  axccd  38938  funimassd  38941  rnmptbddlem  38965  rnmptbd2lem  38974  infnsuprnmpt  38976  rnmptbdlem  38981  upbdrech  39018  ssfiunibd  39022  supxrgere  39048  supxrgelem  39052  supxrge  39053  xralrple2  39069  infxr  39082  infxrunb2  39083  xrralrecnnle  39101  xrralrecnnge  39112  supxrunb3  39122  supxrleubrnmpt  39131  infleinf2  39140  unb2ltle  39141  rexabslelem  39144  suprleubrnmpt  39148  uzub  39157  iccshift  39190  iooshift  39194  iooiinicc  39215  iooiinioc  39229  fsumclf  39237  fsummulc1f  39238  fsumsplit1  39240  fsumf1of  39242  fsumreclf  39244  fsumlessf  39245  fmul01  39248  fmuldfeqlem1  39250  fmuldfeq  39251  fmul01lt1lem1  39252  fmul01lt1lem2  39253  fprodexp  39262  mccl  39266  fprodcnlem  39267  fprodcn  39268  climmulf  39272  climexp  39273  climsuse  39276  climrecf  39277  climinff  39279  climaddf  39283  mullimc  39284  islptre  39287  climf  39290  mullimcf  39291  rexlim2d  39293  idlimc  39294  limcperiod  39296  limcrecl  39297  islpcn  39307  limsupre  39309  limcleqr  39312  addlimc  39316  limclner  39319  climsubmpt  39328  climreclf  39332  climf2  39334  climeldmeqmpt  39336  clim2f2  39338  climfveqmpt  39339  fnlimfvre  39342  allbutfifvre  39343  climleltrp  39344  fnlimf  39346  fnlimabslt  39347  climfveqf  39348  climfveqmpt3  39350  climeldmeqf  39351  climeqf  39356  climeldmeqmpt3  39357  limsuppnfd  39370  limsupub  39372  climinf2lem  39374  climinf2  39375  limsuppnf  39379  limsupubuz  39381  climinf2mpt  39382  climinfmpt  39383  climinf3  39384  limsupmnflem  39388  limsupequz  39391  limsupre2  39393  limsupmnfuzlem  39394  limsupequzmptf  39399  limsupre3  39401  limsupre3uzlem  39403  limsupreuzmpt  39407  supcnvlimsupmpt  39409  cncficcgt0  39436  cncfioobd  39445  fprodsubrecnncnvlem  39456  fprodaddrecnncnvlem  39458  dvmptmulf  39489  dvnmul  39495  dvmptfprodlem  39496  dvmptfprod  39497  dvnprodlem1  39498  dvnprodlem2  39499  iblsplitf  39523  itgperiod  39534  stoweidlem3  39557  stoweidlem26  39580  stoweidlem27  39581  stoweidlem29  39583  stoweidlem31  39585  stoweidlem34  39588  stoweidlem35  39589  stoweidlem36  39590  stoweidlem39  39593  stoweidlem42  39596  stoweidlem43  39597  stoweidlem44  39598  stoweidlem46  39600  stoweidlem48  39602  stoweidlem49  39603  stoweidlem51  39605  stoweidlem52  39606  stoweidlem53  39607  stoweidlem54  39608  stoweidlem55  39609  stoweidlem56  39610  stoweidlem57  39611  stoweidlem58  39612  stoweidlem59  39613  stoweidlem60  39614  stoweidlem61  39615  stoweidlem62  39616  stoweid  39617  wallispilem3  39621  stirlinglem13  39640  stirling  39643  fourierdlem16  39677  fourierdlem21  39682  fourierdlem22  39683  fourierdlem31  39692  fourierdlem39  39700  fourierdlem48  39708  fourierdlem51  39711  fourierdlem53  39713  fourierdlem68  39728  fourierdlem71  39731  fourierdlem73  39733  fourierdlem80  39740  fourierdlem81  39741  fourierdlem86  39746  fourierdlem87  39747  fourierdlem93  39753  fourierdlem94  39754  fourierdlem103  39763  fourierdlem104  39764  fourierdlem112  39772  fourierdlem113  39773  elaa2  39788  etransclem32  39820  salexct  39889  sge0revalmpt  39932  sge0f1o  39936  sge0lefi  39952  sge0resplit  39960  sge0lempt  39964  sge0iunmptlemre  39969  sge0fodjrnlem  39970  sge0iunmpt  39972  sge0ltfirpmpt2  39980  sge0isum  39981  sge0xp  39983  sge0isummpt2  39986  sge0xadd  39989  sge0pnffsumgt  39996  sge0gtfsumgt  39997  sge0uzfsumgt  39998  sge0reuz  40001  sge0reuzb  40002  iundjiun  40014  meadjiun  40020  ismeannd  40021  voliunsge0lem  40026  meaiininc  40038  caragenfiiuncl  40066  omeiunltfirp  40070  ovnsubaddlem2  40122  hoidmvval0  40138  hoidmvlelem1  40146  hoidmvlelem3  40148  hoidmvlelem5  40150  ovnlecvr2  40161  hspdifhsp  40167  hoiqssbllem2  40174  hoiqssbllem3  40175  hspmbllem2  40178  opnvonmbllem2  40184  hoimbl2  40216  vonhoire  40223  iinhoiicc  40225  iunhoiioolem  40226  iunhoiioo  40227  vonioo  40233  vonicc  40236  vonn0ioo2  40241  vonn0icc2  40243  salpreimagelt  40255  salpreimalegt  40257  pimincfltioc  40263  pimdecfgtioo  40264  pimincfltioo  40265  preimageiingt  40267  preimaleiinlt  40268  salpreimagtge  40271  salpreimaltle  40272  salpreimalelt  40275  salpreimagtlt  40276  incsmflem  40287  issmflelem  40290  issmfle  40291  smfconst  40295  issmfgtlem  40301  issmfgt  40302  smfaddlem2  40309  smfadd  40310  decsmflem  40311  decsmf  40312  issmfgelem  40314  issmfge  40315  smflimlem2  40317  smflim  40322  smfresal  40332  smfrec  40333  smfmullem4  40338  smfmul  40339  smfpimcc  40351  smflimmpt  40353  smfsuplem1  40354  smfsupmpt  40358  smfsupxr  40359  smfinflem  40360  smfinfmpt  40362  smflimsuplem5  40367  smflimsuplem7  40369  smflimsuplem8  40370  smflimsupmpt  40372  nfdfat  40544  iccelpart  40697  sprsymrelfo  41065  2zrngmmgm  41264  opeliun2xp  41429  cbvmpt2x2  41432  ovmpt2rdxf  41435  setrec1  41761  aacllem  41880
  Copyright terms: Public domain W3C validator