ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfan Unicode version

Theorem nfan 1565
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 9 . 2  |-  ( ph  ->  F/ x ps )
41, 3nfan1 1564 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 104   F/wnf 1460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  nf3an  1566  cbvex2  1922  nfsbxyt  1943  nfsbv  1947  sbcomxyyz  1972  nfsb4t  2014  clelab  2303  nfel  2328  2ralbida  2498  r19.29an  2619  reean  2645  nfrabxy  2657  cbvrexfw  2695  cbvrexf  2697  cbvreu  2701  cbvrab  2735  ceqsex2  2777  vtocl2gaf  2804  rspce  2836  eqvincf  2862  elrabf  2891  elrab3t  2892  rexab2  2903  morex  2921  reu2  2925  rmo3f  2934  sbc2iegf  3033  rmo2ilem  3052  rmo3  3054  csbiebt  3096  csbie2t  3105  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  nfopd  3793  eluniab  3819  dfnfc2  3825  nfdisjv  3989  disjiun  3995  nfopab  4068  cbvopab  4071  cbvopab1  4073  cbvopab2  4074  cbvopab1s  4075  mpteq12f  4080  nfmpt  4092  cbvmptf  4094  cbvmpt  4095  repizf2  4159  nfpo  4298  nfso  4299  nfwe  4352  onintonm  4513  peano2  4591  nfxp  4650  opeliunxp  4678  nfco  4788  elrnmpt1  4874  nfimad  4975  iota2  5202  dffun4f  5228  nffun  5235  imadif  5292  funimaexglem  5295  nffn  5308  nff  5358  nff1  5415  nffo  5433  nff1o  5455  fun11iun  5478  nffvd  5523  fv3  5534  fmptco  5678  nfiso  5801  cbvriota  5835  riota2df  5845  riota5f  5849  nfoprab  5921  mpoeq123  5928  nfmpo  5938  cbvoprab1  5941  cbvoprab2  5942  cbvoprab12  5943  cbvoprab3  5945  cbvmpox  5947  ovmpodxf  5994  opabex3d  6116  opabex3  6117  dfoprab4f  6188  fmpox  6195  spc2ed  6228  cnvoprab  6229  f1od2  6230  opeliunxp2f  6233  nfrecs  6302  tfri3  6362  nffrec  6391  erovlem  6621  nfixpxy  6711  nfixp1  6712  xpf1o  6838  nneneq  6851  ac6sfi  6892  nfsup  6985  exmidomni  7134  fodjuomnilemdc  7136  ismkvnex  7147  mkvprop  7150  exmidfodomrlemr  7195  exmidfodomrlemrALT  7196  cc3  7255  caucvgsrlemgt1  7782  suplocsrlem  7795  axpre-suploclemres  7888  supinfneg  9581  infsupneg  9582  fimaxre2  11216  nfsum1  11345  nfsum  11346  fsumsplitf  11397  fsum2dlemstep  11423  fsum00  11451  nfcprod1  11543  nfcprod  11544  prodeq2  11546  fprod2dlemstep  11611  fprodsplitf  11621  fprodsplit1f  11623  fprodap0f  11625  fprodle  11629  zsupcllemstep  11926  bezoutlemmain  11979  bezoutlemzz  11983  bezout  11992  exmidunben  12407  ctiunctlemfo  12420  ctiunct  12421  mulcncf  13751  ellimc3apf  13789  limccnp2cntop  13806  bdsepnft  14288  bdsepnfALT  14290  bj-findis  14380  strcollnft  14385  strcollnfALT  14387  pw1nct  14401  isomninnlem  14427  trirec0  14441  iswomninnlem  14446  ismkvnnlem  14449
  Copyright terms: Public domain W3C validator