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

Theorem nfan 1544
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 1543 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 103   F/wnf 1436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487
This theorem depends on definitions:  df-bi 116  df-nf 1437
This theorem is referenced by:  nf3an  1545  cbvex2  1892  nfsbxyt  1914  sbcomxyyz  1943  nfsb4t  1987  clelab  2263  nfel  2288  2ralbida  2454  r19.29an  2572  reean  2597  nfrabxy  2609  cbvrexf  2647  cbvreu  2650  cbvrab  2679  ceqsex2  2721  vtocl2gaf  2748  rspce  2779  eqvincf  2805  elrabf  2833  elrab3t  2834  rexab2  2845  morex  2863  reu2  2867  rmo3f  2876  sbc2iegf  2974  rmo2ilem  2993  rmo3  2995  csbiebt  3034  csbie2t  3043  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  nfopd  3717  eluniab  3743  dfnfc2  3749  nfdisjv  3913  disjiun  3919  nfopab  3991  cbvopab  3994  cbvopab1  3996  cbvopab2  3997  cbvopab1s  3998  mpteq12f  4003  nfmpt  4015  cbvmptf  4017  cbvmpt  4018  repizf2  4081  nfpo  4218  nfso  4219  nfwe  4272  onintonm  4428  peano2  4504  nfxp  4561  opeliunxp  4589  nfco  4699  elrnmpt1  4785  nfimad  4885  iota2  5109  dffun4f  5134  nffun  5141  imadif  5198  funimaexglem  5201  nffn  5214  nff  5264  nff1  5321  nffo  5339  nff1o  5358  fun11iun  5381  nffvd  5426  fv3  5437  fmptco  5579  nfiso  5700  cbvriota  5733  riota2df  5743  riota5f  5747  nfoprab  5816  mpoeq123  5823  nfmpo  5833  cbvoprab1  5836  cbvoprab2  5837  cbvoprab12  5838  cbvoprab3  5840  cbvmpox  5842  ovmpodxf  5889  opabex3d  6012  opabex3  6013  dfoprab4f  6084  fmpox  6091  spc2ed  6123  cnvoprab  6124  f1od2  6125  opeliunxp2f  6128  nfrecs  6197  tfri3  6257  nffrec  6286  erovlem  6514  nfixpxy  6604  nfixp1  6605  xpf1o  6731  nneneq  6744  ac6sfi  6785  nfsup  6872  exmidomni  7007  fodjuomnilemdc  7009  ismkvnex  7022  mkvprop  7025  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  caucvgsrlemgt1  7596  suplocsrlem  7609  axpre-suploclemres  7702  supinfneg  9383  infsupneg  9384  fimaxre2  10991  nfsum1  11118  nfsum  11119  fsumsplitf  11170  fsum2dlemstep  11196  fsum00  11224  nfcprod1  11316  nfcprod  11317  prodeq2  11319  zsupcllemstep  11627  bezoutlemmain  11675  bezoutlemzz  11679  bezout  11688  exmidunben  11928  ctiunctlemfo  11941  ctiunct  11942  mulcncf  12749  ellimc3apf  12787  limccnp2cntop  12804  bdsepnft  13074  bdsepnfALT  13076  bj-findis  13166  strcollnft  13171  isomninnlem  13214
  Copyright terms: Public domain W3C validator