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

Theorem nfan 1956
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  /\  ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
Hypotheses
Ref Expression
nfan.1  |-  F/ x ph
nfan.2  |-  F/ x ps
Assertion
Ref Expression
nfan  |-  F/ x
( ph  /\  ps )

Proof of Theorem nfan
StepHypRef Expression
1 nfan.1 . 2  |-  F/ x ph
2 nfan.2 . . 3  |-  F/ x ps
32a1i 11 . 2  |-  ( ph  ->  F/ x ps )
41, 3nfan1 1955 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367   F/wnf 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-12 1878
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638
This theorem is referenced by:  nfnan  1957  nf3an  1958  hban  1959  nfeqf  2071  nfald2  2099  nfsb4t  2154  2ax6elem  2217  eupicka  2310  mopick2  2313  2mo  2324  2moOLD  2325  2eu6OLD  2335  axbnd  2379  clelab  2546  clelabOLD  2547  nfelOLD  2578  nfabd2  2585  2ralbida  2844  r19.29an  2947  ralcom2  2971  reean  2973  cbvreu  3031  cbvrab  3056  ceqsex2  3096  vtocl2gaf  3123  rspce  3154  eqvincf  3176  elrabf  3204  elrab3t  3205  rexab2  3215  morex  3232  reu2  3236  reu2eqd  3245  sbc2iegf  3343  rmo2  3365  rmo3  3367  csbiebt  3392  csbie2t  3401  cbvreucsf  3406  cbvrabcsf  3407  rabsnifsb  4039  nfop  4174  nfopd  4175  eluniab  4201  dfnfc2  4208  rabasiun  4274  nfopab  4459  cbvopab  4462  cbvopab1  4464  cbvopab2  4465  cbvopab1s  4466  mpteq12f  4470  nfmpt  4482  cbvmptf  4484  cbvmpt  4485  axrep3  4509  axrep4  4510  axrep5  4511  reusv2lem2  4595  reusv2lem3  4596  nfpo  4748  nfso  4749  nffr  4796  nfwe  4798  nfxp  4849  opeliunxp  4874  nfco  4988  elrnmpt1  5071  nfimad  5165  iota2  5558  nffun  5590  imadif  5643  nffn  5657  nff  5709  nff1  5761  nffo  5776  nff1o  5796  nffvd  5857  fv3  5861  fmptco  6042  fsnex  6168  nfiso  6202  nfriotad  6247  cbvriota  6249  riota2df  6259  riota5f  6263  oprabv  6325  nfoprab  6329  mpt2eq123  6336  nfmpt2  6346  cbvoprab1  6349  cbvoprab2  6350  cbvoprab12  6351  cbvoprab3  6353  cbvmpt2x  6355  ovmpt2dxf  6408  elovmpt2rab  6501  elovmpt2rab1  6502  onminex  6624  peano5  6706  fun11iun  6743  opabex3d  6761  opabex3  6762  dfoprab4f  6841  fmpt2x  6849  nfwrecs  7014  wfrlem4  7023  tfr3  7101  tz7.49  7146  erovlem  7443  nfixp  7525  nfixp1  7526  xpf1o  7716  nneneq  7737  ac6sfi  7797  nfoi  7972  wdom2d  8039  infpssrlem4  8717  hsmexlem2  8838  hsmexlem4  8840  domtriomlem  8853  axdc3lem2  8862  axdc4lem  8866  zorn2lem4  8910  zorn2lem5  8911  konigthlem  8974  axextnd  8997  axrepndlem2  8999  axrepnd  9000  axunnd  9002  axpowndlem2  9004  axpowndlem4  9006  axpownd  9007  axregndlem2  9009  axregnd  9010  axregndOLD  9011  axinfndlem1  9012  axinfnd  9013  zfcndrep  9021  zfcndinf  9025  dedekind  9777  dedekindle  9778  fsuppmapnn0fiublem  12138  fsuppmapnn0fiub  12139  fsuppmapnn0fiubex  12140  nfsum1  13659  nfsum  13660  fsum2dlem  13734  fsum00  13761  nfcprod1  13867  nfcprod  13868  fprod2dlem  13934  mreexexd  15260  acsmapd  16130  gsum2d2lem  17320  dprd2d2  17411  gsummoncoe1  18664  gsummatr01lem4  19450  cpmatmcllem  19509  pmatcollpwfi  19573  cayleyhamilton1  19683  neiptopnei  19924  neiptopreu  19925  neitr  19972  iunconlem  20218  iuncon  20219  ptcnplem  20412  ptcnp  20413  xkocnv  20605  isfildlem  20648  utopsnneiplem  21040  isucn2  21072  cfilucfilOLD  21362  cfilucfil  21363  restmetu  21380  ovolfiniun  22202  ovoliunlem3  22205  ovoliunnul  22208  volfiniun  22247  itg2splitlem  22445  itg2split  22446  isibl2  22463  nfitg  22471  cbvitg  22472  limciun  22588  istrkg2ld  24234  chirred  27713  spc2ed  27771  mo5f  27784  rmo3f  27795  rmo4fOLD  27796  foresf1o  27804  cbvdisjf  27850  disjabrex  27860  disjabrexf  27861  elsnxp  27892  funimass4f  27903  fmptcof2  27927  fcomptf  27928  acunirnmpt2  27930  acunirnmpt2f  27931  aciunf1lem  27932  funcnv4mpt  27941  cnvoprab  27979  f1od2  27980  fpwrelmap  27989  xrofsup  28016  nn0min  28049  2sqmo  28075  isarchiofld  28246  reff  28281  locfinreflem  28282  cmpcref  28292  ordtconlem1  28345  esumcl  28463  gsumesum  28492  esumlub  28493  esumcst  28496  esumrnmpt2  28501  esumfzf  28502  esumfsup  28503  hasheuni  28518  esumcvg  28519  esumgect  28523  esumcvgre  28524  esum2dlem  28525  esum2d  28526  esumiun  28527  ldsysgenld  28594  sigapildsyslem  28595  sigapildsys  28596  ldgenpisyslem1  28597  measvunilem  28646  measvunilem0  28647  measvuni  28648  measinblem  28654  voliune  28664  volfiniune  28665  volmeas  28666  oms0  28731  omssubadd  28734  eulerpartlemgvv  28807  dstrvprob  28902  bnj919  29139  bnj1146  29164  bnj1379  29203  bnj849  29297  bnj916  29305  bnj964  29315  bnj1014  29332  bnj1123  29356  bnj1228  29381  bnj1307  29393  bnj1321  29397  bnj1398  29404  bnj1408  29406  bnj1444  29413  bnj1445  29414  bnj1446  29415  bnj1449  29418  bnj1467  29424  bnj1463  29425  bnj1489  29426  bnj1491  29427  bnj1312  29428  bnj1525  29439  cvmcov  29547  iota5f  29918  axextdist  30006  axext4dist  30007  trpredmintr  30032  nfwlim  30065  frrlem4  30077  finminlem  30533  bj-axrep3  30927  bj-axrep4  30928  bj-axrep5  30929  isbasisrelowllem1  31259  isbasisrelowllem2  31260  wl-cbvalnaed  31337  wl-2sb6d  31360  wl-sbalnae  31364  wl-ax11-lem3  31379  heicant  31401  mbfposadd  31414  ftc1anclem5  31447  indexdom  31487  filbcmb  31493  sdclem2  31497  sdclem1  31498  fdc1  31501  riotasv2d  31961  riotasv2s  31962  glbconxN  32375  pmapglb2xN  32769  cdlemefs32sn1aw  33413  mzpsubmpt  35017  mzpexpmpt  35019  eq0rabdioph  35051  eqrabdioph  35052  setindtr  35308  ss2iundf  35618  binomcxplemnotnn0  36089  iunconlem2  36746  elunif  36751  rspcegf  36758  fnchoice  36764  refsumcn  36765  rfcnnnub  36771  upbdrech  36854  ssfiunibd  36858  iccshift  36907  iooshift  36911  fsumclf  36916  fsumsplitf  36917  fsummulc1f  36918  fsumsplit1  36922  fmul01  36923  fmuldfeqlem1  36925  fmuldfeq  36926  fmul01lt1lem1  36927  fmul01lt1lem2  36928  infrglb  36933  fprodsplitf  36938  fprodsplit1f  36942  fprodexp  36949  fprodle  36953  mccl  36955  climmulf  36959  climexp  36960  climsuse  36963  climrecf  36964  climinff  36966  climaddf  36970  mullimc  36971  islptre  36974  climf  36977  mullimcf  36978  rexlim2d  36980  idlimc  36981  limcperiod  36983  limcrecl  36984  islpcn  36994  limsupre  36996  limcleqr  36999  addlimc  37003  limclner  37006  cncficcgt0  37040  cncfioobd  37049  dvmptmulf  37083  dvnmul  37089  dvmptfprodlem  37090  dvmptfprod  37091  dvnprodlem1  37092  dvnprodlem2  37093  iblsplitf  37118  itgperiod  37129  stoweidlem3  37134  stoweidlem26  37157  stoweidlem27  37158  stoweidlem29  37160  stoweidlem31  37162  stoweidlem34  37165  stoweidlem35  37166  stoweidlem36  37167  stoweidlem39  37170  stoweidlem42  37173  stoweidlem43  37174  stoweidlem44  37175  stoweidlem46  37177  stoweidlem48  37179  stoweidlem49  37180  stoweidlem51  37182  stoweidlem52  37183  stoweidlem53  37184  stoweidlem54  37185  stoweidlem55  37186  stoweidlem56  37187  stoweidlem57  37188  stoweidlem58  37189  stoweidlem59  37190  stoweidlem60  37191  stoweidlem61  37192  stoweidlem62  37193  stoweid  37194  wallispilem3  37198  stirlinglem13  37217  stirling  37220  fourierdlem16  37254  fourierdlem21  37259  fourierdlem22  37260  fourierdlem31  37269  fourierdlem39  37277  fourierdlem48  37286  fourierdlem51  37289  fourierdlem53  37291  fourierdlem68  37306  fourierdlem71  37309  fourierdlem73  37311  fourierdlem80  37318  fourierdlem81  37319  fourierdlem86  37324  fourierdlem87  37325  fourierdlem93  37331  fourierdlem94  37332  fourierdlem103  37341  fourierdlem104  37342  fourierdlem112  37350  fourierdlem113  37351  elaa2  37366  etransclem32  37398  nfdfat  37564  iccelpart  37681  2zrngmmgm  38244  opeliun2xp  38414  cbvmpt2x2  38417  ovmpt2rdxf  38420  aacllem  38841
  Copyright terms: Public domain W3C validator