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

Theorem nfan 1783
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  /\  ps ). (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nf.1  |-  F/ x ph
nf.2  |-  F/ x ps
Assertion
Ref Expression
nfan  |-  F/ x
( ph  /\  ps )

Proof of Theorem nfan
StepHypRef Expression
1 df-an 360 . 2  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
2 nf.1 . . . 4  |-  F/ x ph
3 nf.2 . . . . 5  |-  F/ x ps
43nfn 1777 . . . 4  |-  F/ x  -.  ps
52, 4nfim 1781 . . 3  |-  F/ x
( ph  ->  -.  ps )
65nfn 1777 . 2  |-  F/ x  -.  ( ph  ->  -.  ps )
71, 6nfxfr 1560 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   F/wnf 1534
This theorem is referenced by:  nfbi  1784  nf3an  1786  nfeqf  1911  nfald2  1925  spimt  1927  dvelimf  1950  cbval2  1957  cbvex2  1958  nfsb4t  2033  dvelimdf  2035  sbcom  2042  nfeud2  2168  mopick  2218  eupicka  2220  mopick2  2223  2eu6  2241  clelab  2416  nfel  2440  nfabd2  2450  2ralbida  2595  ralcom2  2717  reean  2719  cbvreu  2775  cbvrab  2799  ceqsex2  2837  vtocl2gaf  2863  rspce  2892  eqvincf  2909  elrabf  2935  rexab2  2945  morex  2962  reu2  2966  sbc2iegf  3070  rmo2  3089  rmo3  3091  csbiebt  3130  csbie2t  3138  cbvreucsf  3158  cbvrabcsf  3159  nfop  3828  nfopd  3829  eluniab  3855  dfnfc2  3861  nfopab  4100  cbvopab  4103  cbvopab1  4105  cbvopab2  4106  cbvopab1s  4107  mpteq12f  4112  nfmpt  4124  cbvmpt  4126  axrep3  4150  axrep4  4151  axrep5  4152  nfpo  4335  nfso  4336  nffr  4383  nfwe  4385  reusv2lem2  4552  reusv2lem3  4553  reusv6OLD  4561  onminex  4614  peano5  4695  nfxp  4731  opeliunxp  4756  nfco  4865  elrnmpt1  4944  nfimad  5037  iota2  5261  nffun  5293  imadif  5343  nffn  5356  nff  5403  nff1  5451  nffo  5466  nff1o  5486  fun11iun  5509  nffvd  5550  fv3  5557  fmptco  5707  opabex3  5785  nfiso  5837  nfoprab  5916  mpt2eq123  5923  nfmpt2  5932  cbvoprab1  5934  cbvoprab2  5935  cbvoprab12  5936  cbvoprab3  5938  cbvmpt2x  5940  ovmpt2dxf  5989  dfoprab4f  6194  fmpt2x  6206  nfriotad  6329  cbvriota  6331  riota2df  6341  riota5f  6345  riotasv2d  6365  riotasv2dOLD  6366  riotasv2s  6367  nfrecs  6406  tfr3  6431  tz7.49  6473  erovlem  6770  nfixp  6851  nfixp1  6852  xpf1o  7039  nneneq  7060  ac6sfi  7117  nfoi  7245  wdom2d  7310  infpssrlem4  7948  hsmexlem2  8069  hsmexlem4  8071  domtriomlem  8084  axdc3lem2  8093  axdc4lem  8097  zorn2lem4  8142  zorn2lem5  8143  konigthlem  8206  axextnd  8229  axrepndlem2  8231  axrepnd  8232  axunnd  8234  axpowndlem2  8236  axpowndlem4  8238  axpownd  8239  axregndlem2  8241  axregnd  8242  axinfndlem1  8243  axinfnd  8244  zfcndrep  8252  zfcndinf  8256  nfsum1  12179  nfsum  12180  cbvsum  12184  fsum2dlem  12249  fsum00  12272  mreexexd  13566  acsmapd  14297  gsum2d2lem  15240  dprd2d2  15295  iunconlem  17169  iuncon  17170  ptcnplem  17331  ptcnp  17332  xkocnv  17521  isfildlem  17568  ovolfiniun  18876  ovoliunlem3  18879  ovoliunnul  18882  volfiniun  18920  itg2splitlem  19119  itg2split  19120  isibl2  19137  nfitg  19145  cbvitg  19146  limciun  19260  chirred  22991  funimass4f  23058  mo5f  23159  rmo3f  23194  rmo4fOLD  23195  cbvmptf  23235  fmptcof2  23244  fcomptf  23245  funcnv4mpt  23252  isoun  23257  xrofsup  23270  cbvdisjf  23365  disjabrex  23374  disjabrexf  23375  esumcl  23428  esumcst  23451  hasheuni  23468  esumcvg  23469  measvunilem  23555  measvunilem0  23556  measvuni  23557  measinblem  23562  dstrvprob  23687  cvmcov  23809  dedekind  24097  dedekindle  24098  nfcprod1  24132  nfcprod  24133  axextdist  24227  axext4dist  24228  trpredmintr  24305  wfrlem4  24330  frrlem4  24355  imgfldref2  25167  nfprod1  25413  nfprod  25414  imonclem  25916  ismonc  25917  cmpmon  25918  iepiclem  25926  isepic  25927  lineval22  26185  finminlem  26334  indexdom  26516  filbcmb  26535  sdclem2  26555  sdclem1  26556  fdc1  26559  mzpsubmpt  26924  mzpexpmpt  26926  eq0rabdioph  26959  eqrabdioph  26960  setindtr  27220  elunif  27790  rspcegf  27797  fnchoice  27803  refsumcn  27804  rfcnnnub  27810  fmul01  27813  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  infrglb  27825  climmulf  27833  climexp  27834  climsuse  27837  climrecf  27838  climinff  27840  stoweidlem3  27855  stoweidlem26  27878  stoweidlem27  27879  stoweidlem29  27881  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem36  27888  stoweidlem39  27891  stoweidlem42  27894  stoweidlem43  27895  stoweidlem44  27896  stoweidlem46  27898  stoweidlem48  27900  stoweidlem49  27901  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  stoweidlem55  27907  stoweidlem56  27908  stoweidlem57  27909  stoweidlem58  27910  stoweidlem59  27911  stoweidlem60  27912  stoweidlem61  27913  stoweidlem62  27914  stoweid  27915  wallispilem3  27919  stirlinglem13  27938  stirling  27941  nfdfat  28098  opabex3d  28190  bnj919  29113  bnj1146  29139  bnj1379  29179  bnj849  29273  bnj916  29281  bnj964  29291  bnj1014  29308  bnj1123  29332  bnj1228  29357  bnj1307  29369  bnj1321  29373  bnj1398  29380  bnj1408  29382  bnj1444  29389  bnj1445  29390  bnj1446  29391  bnj1449  29394  bnj1467  29400  bnj1463  29401  bnj1489  29402  bnj1491  29403  bnj1312  29404  bnj1525  29415  nfeqfNEW7  29463  spimtNEW7  29484  nfsb4twAUX7  29551  sbcomwAUX7  29562  nfald2OLD7  29671  dvelimfOLD7  29681  cbval2OLD7  29684  cbvex2OLD7  29685  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  dvelimdfOLD7  29705  sbcomOLD7  29709  a12lem1  29752  a12study  29754  glbconxN  30189  pmapglb2xN  30583  cdlemefs32sn1aw  31225
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-nf 1535
  Copyright terms: Public domain W3C validator