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

Theorem nfan 1771
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 1765 . . . 4  |-  F/ x  -.  ps
52, 4nfim 1769 . . 3  |-  F/ x
( ph  ->  -.  ps )
65nfn 1765 . 2  |-  F/ x  -.  ( ph  ->  -.  ps )
71, 6nfxfr 1557 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358   F/wnf 1531
This theorem is referenced by:  nfbi  1772  nf3an  1774  nfeqf  1898  nfald2  1912  spimt  1914  dvelimf  1937  cbval2  1944  cbvex2  1945  nfsb4t  2020  dvelimdf  2022  sbcom  2029  nfeud2  2155  mopick  2205  eupicka  2207  mopick2  2210  2eu6  2228  clelab  2403  nfel  2427  nfabd2  2437  2ralbida  2582  ralcom2  2704  reean  2706  cbvreu  2762  cbvrab  2786  ceqsex2  2824  vtocl2gaf  2850  rspce  2879  eqvincf  2896  elrabf  2922  rexab2  2932  morex  2949  reu2  2953  sbc2iegf  3057  rmo2  3076  rmo3  3078  csbiebt  3117  csbie2t  3125  cbvreucsf  3145  cbvrabcsf  3146  nfop  3812  nfopd  3813  eluniab  3839  dfnfc2  3845  nfopab  4084  cbvopab  4087  cbvopab1  4089  cbvopab2  4090  cbvopab1s  4091  mpteq12f  4096  nfmpt  4108  cbvmpt  4110  axrep3  4134  axrep4  4135  axrep5  4136  nfpo  4319  nfso  4320  nffr  4367  nfwe  4369  reusv2lem2  4536  reusv2lem3  4537  reusv6OLD  4545  onminex  4598  peano5  4679  nfxp  4715  opeliunxp  4740  nfco  4849  elrnmpt1  4928  nfimad  5021  iota2  5245  nffun  5277  imadif  5327  nffn  5340  nff  5387  nff1  5435  nffo  5450  nff1o  5470  fun11iun  5493  nffvd  5534  fv3  5541  fmptco  5691  opabex3  5769  nfiso  5821  nfoprab  5900  mpt2eq123  5907  nfmpt2  5916  cbvoprab1  5918  cbvoprab2  5919  cbvoprab12  5920  cbvoprab3  5922  cbvmpt2x  5924  ovmpt2dxf  5973  dfoprab4f  6178  fmpt2x  6190  nfriotad  6313  cbvriota  6315  riota2df  6325  riota5f  6329  riotasv2d  6349  riotasv2dOLD  6350  riotasv2s  6351  nfrecs  6390  tfr3  6415  tz7.49  6457  erovlem  6754  nfixp  6835  nfixp1  6836  xpf1o  7023  nneneq  7044  ac6sfi  7101  nfoi  7229  wdom2d  7294  infpssrlem4  7932  hsmexlem2  8053  hsmexlem4  8055  domtriomlem  8068  axdc3lem2  8077  axdc4lem  8081  zorn2lem4  8126  zorn2lem5  8127  konigthlem  8190  axextnd  8213  axrepndlem2  8215  axrepnd  8216  axunnd  8218  axpowndlem2  8220  axpowndlem4  8222  axpownd  8223  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axinfnd  8228  zfcndrep  8236  zfcndinf  8240  nfsum1  12163  nfsum  12164  cbvsum  12168  fsum2dlem  12233  fsum00  12256  mreexexd  13550  acsmapd  14281  gsum2d2lem  15224  dprd2d2  15279  iunconlem  17153  iuncon  17154  ptcnplem  17315  ptcnp  17316  xkocnv  17505  isfildlem  17552  ovolfiniun  18860  ovoliunlem3  18863  ovoliunnul  18866  volfiniun  18904  itg2splitlem  19103  itg2split  19104  isibl2  19121  nfitg  19129  cbvitg  19130  limciun  19244  chirred  22975  funimass4f  23042  mo5f  23143  rmo3f  23178  rmo4fOLD  23179  cbvmptf  23220  fmptcof2  23229  fcomptf  23230  funcnv4mpt  23237  isoun  23242  xrofsup  23255  cbvdisjf  23350  disjabrex  23359  disjabrexf  23360  esumcl  23413  esumcst  23436  hasheuni  23453  esumcvg  23454  measvunilem  23540  measvunilem0  23541  measvuni  23542  measinblem  23547  dstrvprob  23672  cvmcov  23794  dedekind  24082  dedekindle  24083  axextdist  24156  axext4dist  24157  trpredmintr  24234  wfrlem4  24259  frrlem4  24284  imgfldref2  25064  nfprod1  25310  nfprod  25311  imonclem  25813  ismonc  25814  cmpmon  25815  iepiclem  25823  isepic  25824  lineval22  26082  finminlem  26231  indexdom  26413  filbcmb  26432  sdclem2  26452  sdclem1  26453  fdc1  26456  mzpsubmpt  26821  mzpexpmpt  26823  eq0rabdioph  26856  eqrabdioph  26857  setindtr  27117  elunif  27687  rspcegf  27694  fnchoice  27700  refsumcn  27701  rfcnnnub  27707  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  infrglb  27722  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  climinff  27737  stoweidlem3  27752  stoweidlem26  27775  stoweidlem27  27776  stoweidlem29  27778  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem36  27785  stoweidlem39  27788  stoweidlem42  27791  stoweidlem43  27792  stoweidlem44  27793  stoweidlem46  27795  stoweidlem48  27797  stoweidlem49  27798  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem55  27804  stoweidlem56  27805  stoweidlem57  27806  stoweidlem58  27807  stoweidlem59  27808  stoweidlem60  27809  stoweidlem61  27810  stoweidlem62  27811  stoweid  27812  wallispilem3  27816  stirlinglem13  27835  stirling  27838  nfdfat  27993  bnj919  28797  bnj1146  28823  bnj1379  28863  bnj849  28957  bnj916  28965  bnj964  28975  bnj1014  28992  bnj1123  29016  bnj1228  29041  bnj1307  29053  bnj1321  29057  bnj1398  29064  bnj1408  29066  bnj1444  29073  bnj1445  29074  bnj1446  29075  bnj1449  29078  bnj1467  29084  bnj1463  29085  bnj1489  29086  bnj1491  29087  bnj1312  29088  bnj1525  29099  a12lem1  29130  a12study  29132  glbconxN  29567  pmapglb2xN  29961  cdlemefs32sn1aw  30603
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-nf 1532
  Copyright terms: Public domain W3C validator