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

Theorem nfan 1983
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 1982 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-12 1904
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664
This theorem is referenced by:  nfnan  1984  nf3an  1985  hban  1986  nfeqf  2098  nfald2  2126  nfsb4t  2181  2ax6elem  2242  eupicka  2331  mopick2  2334  2mo  2345  2moOLD  2346  axbnd  2397  clelab  2564  clelabOLD  2565  nfelOLD  2596  nfabd2  2603  2ralbida  2864  r19.29an  2967  ralcom2  2991  reean  2993  cbvreu  3051  cbvrab  3076  ceqsex2  3116  vtocl2gaf  3143  rspce  3174  eqvincf  3196  elrabf  3224  elrab3t  3225  rexab2  3235  morex  3252  reu2  3256  reu2eqd  3265  sbc2iegf  3363  rmo2  3385  rmo3  3387  csbiebt  3412  csbie2t  3421  cbvreucsf  3426  cbvrabcsf  3427  rabsnifsb  4062  nfop  4197  nfopd  4198  eluniab  4224  dfnfc2  4231  rabasiun  4297  nfopab  4483  cbvopab  4486  cbvopab1  4488  cbvopab2  4489  cbvopab1s  4490  mpteq12f  4494  nfmpt  4506  cbvmptf  4508  cbvmpt  4509  axrep3  4533  axrep4  4534  axrep5  4535  reusv2lem2  4619  reusv2lem3  4620  nfpo  4772  nfso  4773  nffr  4820  nfwe  4822  nfxp  4873  opeliunxp  4898  nfco  5012  elrnmpt1  5095  nfimad  5189  iota2  5583  nffun  5615  imadif  5668  nffn  5682  nff  5734  nff1  5786  nffo  5801  nff1o  5821  nffvd  5882  fv3  5886  fmptco  6063  fsnex  6188  nfiso  6222  nfriotad  6267  cbvriota  6269  riota2df  6279  riota5f  6283  oprabv  6345  nfoprab  6349  mpt2eq123  6356  nfmpt2  6366  cbvoprab1  6369  cbvoprab2  6370  cbvoprab12  6371  cbvoprab3  6373  cbvmpt2x  6375  ovmpt2dxf  6428  elovmpt2rab  6521  elovmpt2rab1  6522  onminex  6640  peano5  6722  fun11iun  6759  opabex3d  6777  opabex3  6778  dfoprab4f  6857  fmpt2x  6865  nfwrecs  7030  wfrlem4  7039  tfr3  7117  tz7.49  7162  erovlem  7459  nfixp  7541  nfixp1  7542  xpf1o  7732  nneneq  7753  ac6sfi  7813  nfoi  8027  wdom2d  8093  infpssrlem4  8732  hsmexlem2  8853  hsmexlem4  8855  domtriomlem  8868  axdc3lem2  8877  axdc4lem  8881  zorn2lem4  8925  zorn2lem5  8926  konigthlem  8989  axextnd  9012  axrepndlem2  9014  axrepnd  9015  axunnd  9017  axpowndlem2  9019  axpowndlem4  9021  axpownd  9022  axregndlem2  9024  axregnd  9025  axinfndlem1  9026  axinfnd  9027  zfcndrep  9035  zfcndinf  9039  dedekind  9793  dedekindle  9794  fsuppmapnn0fiublem  12195  fsuppmapnn0fiub  12196  fsuppmapnn0fiubex  12197  nfsum1  13734  nfsum  13735  fsum2dlem  13809  fsum00  13836  nfcprod1  13942  nfcprod  13943  fprod2dlem  14012  fprodsplitf  14020  fprodsplit1f  14022  fprodle  14028  lcmfunsnlem1  14588  lcmfunsnlem2lem1  14589  lcmfunsnlem2  14591  mreexexd  15532  acsmapd  16402  gsum2d2lem  17583  dprd2d2  17655  gsummoncoe1  18876  gsummatr01lem4  19660  cpmatmcllem  19719  pmatcollpwfi  19783  cayleyhamilton1  19893  neiptopnei  20125  neiptopreu  20126  neitr  20173  iunconlem  20419  iuncon  20420  ptcnplem  20613  ptcnp  20614  xkocnv  20806  isfildlem  20849  utopsnneiplem  21239  isucn2  21271  cfilucfil  21551  restmetu  21562  ovolfiniun  22431  ovoliunlem3  22434  ovoliunnul  22437  volfiniun  22477  itg2splitlem  22683  itg2split  22684  isibl2  22701  nfitg  22709  cbvitg  22710  limciun  22826  istrkg2ld  24485  chirred  28024  spc2ed  28082  mo5f  28096  rmo3f  28107  rmo4fOLD  28108  foresf1o  28116  cbvdisjf  28162  disjabrex  28172  disjabrexf  28173  elsnxp  28204  funimass4f  28215  fmptcof2  28240  fcomptf  28241  acunirnmpt2  28243  acunirnmpt2f  28244  aciunf1lem  28245  funcnv4mpt  28254  cnvoprab  28293  f1od2  28294  fpwrelmap  28303  xrofsup  28338  nn0min  28371  2sqmo  28397  isarchiofld  28569  reff  28655  locfinreflem  28656  cmpcref  28666  ordtconlem1  28719  esumcl  28840  gsumesum  28869  esumlub  28870  esumcst  28873  esumrnmpt2  28878  esumfzf  28879  esumfsup  28880  hasheuni  28895  esumcvg  28896  esumgect  28900  esumcvgre  28901  esum2dlem  28902  esum2d  28903  esumiun  28904  ldsysgenld  28971  sigapildsyslem  28972  sigapildsys  28973  ldgenpisyslem1  28974  measvunilem  29023  measvunilem0  29024  measvuni  29025  measinblem  29031  voliune  29041  volfiniune  29042  volmeas  29043  oms0  29114  omssubadd  29117  oms0OLD  29118  omssubaddOLD  29121  eulerpartlemgvv  29198  dstrvprob  29293  bnj919  29567  bnj1146  29592  bnj1379  29631  bnj849  29725  bnj916  29733  bnj964  29743  bnj1014  29760  bnj1123  29784  bnj1228  29809  bnj1307  29821  bnj1321  29825  bnj1398  29832  bnj1408  29834  bnj1444  29841  bnj1445  29842  bnj1446  29843  bnj1449  29846  bnj1467  29852  bnj1463  29853  bnj1489  29854  bnj1491  29855  bnj1312  29856  bnj1525  29867  cvmcov  29975  iota5f  30346  axextdist  30434  axext4dist  30435  trpredmintr  30460  nfwlim  30493  frrlem4  30505  finminlem  30960  bj-axrep3  31357  bj-axrep4  31358  bj-axrep5  31359  isbasisrelowllem1  31693  isbasisrelowllem2  31694  wl-cbvalnaed  31773  wl-2sb6d  31796  wl-sbalnae  31800  wl-mo2tf  31808  wl-eutf  31810  wl-ax11-lem3  31825  phpreu  31837  poimirlem26  31874  poimirlem27  31875  heicant  31883  mbfposadd  31896  ftc1anclem5  31929  indexdom  31969  filbcmb  31975  sdclem2  31979  sdclem1  31980  fdc1  31983  riotasv2d  32442  riotasv2s  32443  glbconxN  32856  pmapglb2xN  33250  cdlemefs32sn1aw  33894  mzpsubmpt  35498  mzpexpmpt  35500  eq0rabdioph  35532  eqrabdioph  35533  setindtr  35793  ss2iundf  36105  binomcxplemnotnn0  36557  iunconlem2  37187  elunif  37192  rspcegf  37199  fnchoice  37205  refsumcn  37206  rfcnnnub  37212  uzwo4  37248  fiiuncl  37263  disjf1  37295  wessf1ornlem  37297  disjrnmpt2  37301  disjf1o  37304  fompt  37305  disjinfi  37306  upbdrech  37347  ssfiunibd  37351  supxrgere  37380  supxrgelem  37384  supxrge  37385  iccshift  37419  iooshift  37423  fsumclf  37435  fsumsplitf  37436  fsummulc1f  37437  fsumsplit1  37441  fsumf1of  37443  fmul01  37445  fmuldfeqlem1  37447  fmuldfeq  37448  fmul01lt1lem1  37449  fmul01lt1lem2  37450  infrglbOLD  37456  fprodexp  37461  mccl  37465  climmulf  37469  climexp  37470  climsuse  37474  climrecf  37475  climinff  37477  climinffOLD  37478  climaddf  37482  mullimc  37483  islptre  37486  climf  37489  mullimcf  37490  rexlim2d  37492  idlimc  37493  limcperiod  37495  limcrecl  37496  islpcn  37506  limsupre  37508  limsupreOLD  37509  limcleqr  37512  addlimc  37516  limclner  37519  cncficcgt0  37553  cncfioobd  37562  dvmptmulf  37599  dvnmul  37605  dvmptfprodlem  37606  dvmptfprod  37607  dvnprodlem1  37608  dvnprodlem2  37609  iblsplitf  37634  itgperiod  37645  stoweidlem3  37650  stoweidlem26  37673  stoweidlem27  37674  stoweidlem29  37676  stoweidlem29OLD  37677  stoweidlem31  37679  stoweidlem34  37682  stoweidlem35  37683  stoweidlem36  37684  stoweidlem39  37687  stoweidlem42  37690  stoweidlem43  37691  stoweidlem44  37692  stoweidlem46  37694  stoweidlem48  37696  stoweidlem49  37697  stoweidlem51  37699  stoweidlem52  37700  stoweidlem53  37701  stoweidlem54  37702  stoweidlem55  37703  stoweidlem56  37704  stoweidlem57  37705  stoweidlem58  37706  stoweidlem59  37707  stoweidlem60  37708  stoweidlem61  37709  stoweidlem62  37710  stoweidlem62OLD  37711  stoweid  37712  wallispilem3  37716  stirlinglem13  37735  stirling  37738  fourierdlem16  37772  fourierdlem21  37777  fourierdlem22  37778  fourierdlem31  37787  fourierdlem31OLD  37788  fourierdlem39  37796  fourierdlem48  37805  fourierdlem51  37808  fourierdlem53  37810  fourierdlem68  37825  fourierdlem71  37828  fourierdlem73  37830  fourierdlem80  37837  fourierdlem81  37838  fourierdlem86  37843  fourierdlem87  37844  fourierdlem93  37850  fourierdlem94  37851  fourierdlem103  37860  fourierdlem104  37861  fourierdlem112  37869  fourierdlem113  37870  elaa2  37886  etransclem32  37918  sge0revalmpt  37975  sge0f1o  37979  sge0lefi  37995  sge0resplit  38003  sge0lempt  38007  sge0iunmptlemre  38012  sge0fodjrnlem  38013  sge0iunmpt  38015  iundjiun  38028  meadjiun  38034  ismeannd  38035  caragenfiiuncl  38066  omeiunltfirp  38070  nfdfat  38252  iccelpart  38367  2zrngmmgm  39008  opeliun2xp  39178  cbvmpt2x2  39181  ovmpt2rdxf  39184  aacllem  39605
  Copyright terms: Public domain W3C validator